OAI/Geometry/CAT0Fillings/Calculus/Truncation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ClosedCalculus.min_const_deriv_low line 14
2. lemma OAI.CAT0Fillings.ClosedCalculus.min_const_deriv_high line 19
3. lemma OAI.CAT0Fillings.ClosedCalculus.min_const_lipschitz line 24
4. lemma OAI.CAT0Fillings.ChartGeometry.closed_min_const line 33
5. lemma OAI.CAT0Fillings.ClosedCalculus.max_const_deriv_low line 62
6. lemma OAI.CAT0Fillings.ClosedCalculus.max_const_deriv_high line 67
7. lemma OAI.CAT0Fillings.ClosedCalculus.max_const_lipschitz line 72
8. lemma OAI.CAT0Fillings.ChartGeometry.closed_max_const line 81