OAI/Geometry/CylinderCovering/Cartesian/Caps.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.CartesianCaps.D_nonneg line 9
2. lemma OAI.CylinderCovering.CartesianCaps.D_le line 13
3. lemma OAI.CylinderCovering.CartesianCaps.D_sub_factor line 19
4. lemma OAI.CylinderCovering.CartesianCaps.D_lipschitz line 24
5. lemma OAI.CylinderCovering.CartesianCaps.abs_mul_le_one line 38
6. lemma OAI.CylinderCovering.CartesianCaps.D_ray_lipschitz line 45
7. lemma OAI.CylinderCovering.CartesianCaps.small_square line 57
8. lemma OAI.CylinderCovering.CartesianCaps.residual_strictMono line 60
9. lemma OAI.CylinderCovering.CartesianCaps.root_exists line 72
10. lemma OAI.CylinderCovering.CartesianCaps.cap_spec line 93
11. lemma OAI.CylinderCovering.CartesianCaps.cap_equation line 101
12. lemma OAI.CylinderCovering.CartesianCaps.cap_mem_unit line 108
13. lemma OAI.CylinderCovering.CartesianCaps.cap_unique line 114
14. lemma OAI.CylinderCovering.CartesianCaps.residual_nonpos_iff line 121
15. lemma OAI.CylinderCovering.CartesianCaps.aperture_eq_Icc line 138
16. lemma OAI.CylinderCovering.CartesianCaps.cap_lipschitz line 155
17. lemma OAI.CylinderCovering.CartesianCaps.cap_continuousOn line 190
18. lemma OAI.CylinderCovering.CartesianCaps.D_half line 199
19. lemma OAI.CylinderCovering.CartesianCaps.cap_quadratic_bound line 203
20. lemma OAI.CylinderCovering.CartesianCaps.cap_fourth_order line 214
21. theorem OAI.CylinderCovering.CartesianCaps.cap_properties line 231