OAI/Geometry/SurfaceImmersion/Atlas/PhaseMarginCompact.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A relative normal-length margin places every relevant point in a fixed compact noncritical region, before the immersion or its fast scale is selected.

  1. def OAI.ClosedSurfaceR4.PhaseGeometry.phaseMarginCompact line 16
  2. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseMarginCompact_noncritical line 22
  3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.mem_phaseMarginCompact_of_relative_margin line 31
  4. theorem OAI.ClosedSurfaceR4.PhaseGeometry.fixed_margin_phase_partition line 38