OAI/Geometry/Immersion/ClosedSurface/LocalPhaseData.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.PhaseGeometry.smooth_extension_near line 20
2. lemma OAI.ClosedSurfaceR4.RealModes.coordDeriv_eventuallyEq line 42
3. lemma OAI.ClosedSurfaceR4.RealModes.realSecondForm_eventuallyEq line 47
4. lemma OAI.ClosedSurfaceR4.RealModes.realSecondTensor_eventuallyEq line 54
5. theorem OAI.ClosedSurfaceR4.RealModes.actual_local_phase_data_on line 64