OAI/Geometry/Immersion/ClosedSurface/UniformIncrement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.RealModes.FreeBudget.shrink line 15
2. def OAI.ClosedSurfaceR4.RealModes.ForcedGeometryBudget.shrink line 21
3. lemma OAI.ClosedSurfaceR4.RealModes.FreeBudget.factors_eq line 27
4. theorem OAI.ClosedSurfaceR4.RealModes.constructed_finite_increment_uniform line 39
5. lemma OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor_congr_left line 90
6. lemma OAI.ClosedSurfaceR4.RealModes.phaseZeroTensor_supported_phase line 98
7. lemma OAI.ClosedSurfaceR4.RealModes.SupportedFreeChart.mean_phase line 112