OAI/Geometry/SurfaceImmersion/Primitive/PeriodicSupport.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Support preservation for the actual finite periodic expansion.

  1. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.periodic_family_flat_on_closure line 21
  2. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.finiteAnsatz_eq_base_of_zero line 32
  3. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.metricCoefficientFamily_zero_of_positive_coefficients line 39
  4. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.initial_zero_of_constant line 64
  5. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.xTangent_zero_on line 76
  6. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.yTangent_zero_on line 86
  7. lemma OAI.ClosedSurfaceR4.PeriodicExpansion.Geometry.remainders_zero_on line 93