OAI/Geometry/Immersion/ClosedSurface/MetricBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ClosedSurfaceR4.coordinateInverse_mfderiv_injective line 14
2. lemma OAI.ClosedSurfaceR4.coordinateMetric_continuousOn line 43
3. lemma OAI.ClosedSurfaceR4.coordinateMetric_positive line 49
4. theorem OAI.ClosedSurfaceR4.coordinateMetric_compact_positive line 60
5. lemma OAI.ClosedSurfaceR4.metricPullback_smoothOn line 78
6. lemma OAI.ClosedSurfaceR4.coordinateMetric_smoothOn line 97
7. theorem OAI.ClosedSurfaceR4.coordinateMetric_ball_bounds line 112
8. theorem OAI.ClosedSurfaceR4.finite_atlas_metric_bounds line 146