OAI/Geometry/Immersion/ClosedSurface/PhaseStock.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.compact_finite_uniform_margin line 15
2. structure OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis line 47
3. abbrev OAI.ClosedSurfaceR4.PhaseGeometry.PhaseInput line 53
4. def OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis.margin line 55
5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis.margin_lt_iff line 59
6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.PhaseBasis.margin_continuous line 64
7. lemma OAI.ClosedSurfaceR4.PhaseGeometry.positive_input_has_basis line 71
8. theorem OAI.ClosedSurfaceR4.PhaseGeometry.compact_positive_phase_bases line 82
9. lemma OAI.ClosedSurfaceR4.PhaseGeometry.secondQuadratic_smul_form line 102
10. lemma OAI.ClosedSurfaceR4.PhaseGeometry.good_smul_form_iff line 108
11. theorem OAI.ClosedSurfaceR4.PhaseGeometry.normalized_positive_phase_bases line 119
12. theorem OAI.ClosedSurfaceR4.PhaseGeometry.uniform_normalized_phase_margin line 149