OAI/Geometry/Immersion/ClosedSurface/FiniteMean.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ClosedSurfaceR4.FiniteMean.InTrialBall line 17
2. def OAI.ClosedSurfaceR4.FiniteMean.trial line 21
3. structure OAI.ClosedSurfaceR4.FiniteMean.MeanBounds line 29
4. def OAI.ClosedSurfaceR4.FiniteMean.sizeBound line 47
5. def OAI.ClosedSurfaceR4.FiniteMean.differenceBound line 51
6. lemma OAI.ClosedSurfaceR4.FiniteMean.sizeBound_ge_one line 56
7. lemma OAI.ClosedSurfaceR4.FiniteMean.differenceBound_nonneg line 66
8. lemma OAI.ClosedSurfaceR4.FiniteMean.finite_upper line 77
9. lemma OAI.ClosedSurfaceR4.FiniteMean.trial_difference line 96
10. lemma OAI.ClosedSurfaceR4.FiniteMean.trial_residual line 104
11. theorem OAI.ClosedSurfaceR4.FiniteMean.finite_substitution line 115