OAI/Geometry/IsometricImmersion/Calculus/MetricInverseJetBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothLocal.Geometry.metricQuotientNumeratorBound line 12
2. def OAI.SmoothLocal.Geometry.metricInverseJetBound line 13
3. theorem OAI.SmoothLocal.Geometry.metricInverseJetBound_nonneg line 16
4. theorem OAI.SmoothLocal.Geometry.metricDet_coordinate_bound line 25
5. theorem OAI.SmoothLocal.Geometry.metricAdjugate_coordinate_bound line 36
6. theorem OAI.SmoothLocal.Geometry.inverseMetric_eq_adjugate_div line 46
7. theorem OAI.SmoothLocal.Geometry.inverseMetric_coordinate_bound line 51