structure definition def or abbrev

`FlatSimplicialComplex`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  73structure FlatSimplicialComplex (nH nE : ℕ) where
  74  hinges : Fin nH → SimplicialHingeData
  75  edges_length_flat : Fin nE → ℝ
  76  edges_length_pos : ∀ e, 0 < edges_length_flat e
  77  flat_all : ∀ h : Fin nH,
  78    DihedralAngle.FlatSumCondition (hinges h).dihedrals
  79
  80/-- A perturbation of the flat edge-lengths. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

WellShapedData in IndisputableMonolith.Geometry.DeficitLinearization decl_use

depends on (10)

Lean names referenced from this declaration's body.

of in IndisputableMonolith.Astrophysics.NucleosynthesisTiers decl_use
of in IndisputableMonolith.Foundation.DAlembert.LedgerFactorization decl_use
A in IndisputableMonolith.Foundation.IntegrationGap decl_use
of in IndisputableMonolith.Foundation.PhiForcingDerived decl_use
of in IndisputableMonolith.Foundation.SpectralEmergence decl_use
FlatSumCondition in IndisputableMonolith.Geometry.DihedralAngle decl_use
SimplicialHingeData in IndisputableMonolith.Geometry.Schlaefli decl_use
of in IndisputableMonolith.Information.PhysicsComplexityStructure decl_use
A in IndisputableMonolith.Masses.Anchor decl_use
A in IndisputableMonolith.Modal.Actualization decl_use