OAI/Geometry/Immersion/ClosedSurface/GoodPhases.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.PhaseGeometry.good_weighted line 13
2. theorem OAI.ClosedSurfaceR4.PhaseGeometry.positive_good_slopes line 25
3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.good_neg line 76
4. theorem OAI.ClosedSurfaceR4.PhaseGeometry.positive_good_phase_data line 85
5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.continuous_secondQuadratic line 147
6. lemma OAI.ClosedSurfaceR4.PhaseGeometry.isOpen_good line 152
7. theorem OAI.ClosedSurfaceR4.PhaseGeometry.positive_good_local_data line 163