OAI/Geometry/Immersion/ClosedSurface/Main.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.space_inner_eq_sum line 15
2. theorem OAI.ClosedSurfaceR4.IsSmoothIsometricImmersion.mfderiv_injective line 24
3. theorem OAI.ClosedSurfaceR4.PhaseGeometry.positive_tensor_has_basis line 38
4. theorem OAI.ClosedSurfaceR4.exists_positive_metric_phase_neighborhood line 72
5. theorem OAI.ClosedSurfaceR4.exists_finite_tangent_metric_decomposition line 100