OAI/Geometry/Immersion/ClosedSurface/ImmersionJets.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.RealModes.gramDet_ne_zero_of_injective line 15
2. lemma OAI.ClosedSurfaceR4.RealModes.injective_of_gramDet_ne_zero line 37
3. lemma OAI.ClosedSurfaceR4.RealModes.gramDet_ne_zero_iff_injective line 61
4. lemma OAI.ClosedSurfaceR4.RealModes.contDiffAt_realSecondTensor line 70
5. lemma OAI.ClosedSurfaceR4.RealModes.continuous_gramDet_field line 85
6. lemma OAI.ClosedSurfaceR4.RealModes.good_eventually line 92
7. theorem OAI.ClosedSurfaceR4.RealModes.actual_local_phase_data line 103