OAI/Geometry/Immersion/ClosedSurface/FreeSolve.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ClosedSurfaceR4.RealModes.real_finite_free_mode line 18
2. theorem OAI.ClosedSurfaceR4.RealModes.weighted_chart_free line 69
3. lemma OAI.ClosedSurfaceR4.RealModes.realLinearizedTensor_indicator line 132
4. lemma OAI.ClosedSurfaceR4.RealModes.displacement_indicator line 148
5. theorem OAI.ClosedSurfaceR4.RealModes.weighted_extended_chart_free line 160