OAI/Geometry/SurfaceImmersion/Atlas/CompactPhaseFamily.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Retain the geometric charts when constructing the compact target split.

  1. structure OAI.ClosedSurfaceR4.PhaseGeometry.CompactPhaseFamily line 15
  2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_compactPhaseFamily line 21
  3. def OAI.ClosedSurfaceR4.PhaseGeometry.CompactPhaseFamily.support line 40
  4. def OAI.ClosedSurfaceR4.PhaseGeometry.CompactPhaseFamily.split line 43
  5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.CompactPhaseFamily.support_subset line 47
  6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.CompactPhaseFamily.support_chart line 50
  7. lemma OAI.ClosedSurfaceR4.PhaseGeometry.CompactPhaseFamily.split_sum line 54
  8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.CompactPhaseFamily.split_bound line 57