OAI/Geometry/Immersion/ClosedSurface/PhaseCoordinates.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.PhaseGeometry.phaseCoframe line 14
2. def OAI.ClosedSurfaceR4.PhaseGeometry.phaseCoframeInv line 19
3. lemma OAI.ClosedSurfaceR4.PhaseGeometry.covector_length_sq_pos line 25
4. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseCoframe_left_inv line 31
5. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseCoframe_right_inv line 38
6. def OAI.ClosedSurfaceR4.PhaseGeometry.phaseEquiv line 45
7. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseEquiv_apply line 50
8. lemma OAI.ClosedSurfaceR4.PhaseGeometry.phaseEquiv_symm_apply line 53
9. theorem OAI.ClosedSurfaceR4.PhaseGeometry.exists_phase_complement line 58