OAI/Geometry/Immersion/ClosedSurface/JacobianBounds.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.RealModes.coordDet_comp line 12
2. lemma OAI.ClosedSurfaceR4.RealModes.coordDet_id line 19
3. lemma OAI.ClosedSurfaceR4.RealModes.continuous_coordDet line 22
4. lemma OAI.ClosedSurfaceR4.RealModes.coordDet_fderiv_ne_zero_of_local_inverse line 26
5. theorem OAI.ClosedSurfaceR4.RealModes.compact_chart_jacobian_bounds line 45