OAI/Geometry/CylinderCovering/Angular/OrdinaryCaps.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.AngularOrdinaryCaps.interval_abs_le line 10
2. lemma OAI.CylinderCovering.AngularOrdinaryCaps.profile_lipschitz line 14
3. lemma OAI.CylinderCovering.AngularOrdinaryCaps.profile_le_max_endpoints line 32
4. lemma OAI.CylinderCovering.AngularOrdinaryCaps.maximumProfile_eq_sSup line 52
5. lemma OAI.CylinderCovering.AngularOrdinaryCaps.shared_left line 71
6. lemma OAI.CylinderCovering.AngularOrdinaryCaps.shared_right line 76
7. lemma OAI.CylinderCovering.AngularOrdinaryCaps.secantBeta_error line 81
8. lemma OAI.CylinderCovering.AngularOrdinaryCaps.secantAlpha_error line 87
9. lemma OAI.CylinderCovering.AngularOrdinaryCaps.profile_cell_error line 104
10. lemma OAI.CylinderCovering.AngularOrdinaryCaps.max_profile_cell_error line 113
11. lemma OAI.CylinderCovering.AngularOrdinaryCaps.taggedRadius_error line 126
12. lemma OAI.CylinderCovering.AngularOrdinaryCaps.midpointRadius_error line 139
13. lemma OAI.CylinderCovering.AngularOrdinaryCaps.maximumRadius_error line 146
14. lemma OAI.CylinderCovering.AngularOrdinaryCaps.radialRadius_error line 159
15. lemma OAI.CylinderCovering.AngularOrdinaryCaps.taggedRadius_pos line 163
16. lemma OAI.CylinderCovering.AngularOrdinaryCaps.midpointRadius_pos line 167
17. lemma OAI.CylinderCovering.AngularOrdinaryCaps.maximumRadius_pos line 170
18. lemma OAI.CylinderCovering.AngularOrdinaryCaps.continuous_radialRadius line 176
19. theorem OAI.CylinderCovering.AngularOrdinaryCaps.ordinary_cell_estimates line 180
20. lemma OAI.CylinderCovering.AngularOrdinaryCaps.exists_continuous_gluing line 196
21. lemma OAI.CylinderCovering.AngularOrdinaryCaps.exists_secant_boundary line 246
22. theorem OAI.CylinderCovering.AngularOrdinaryCaps.ordinaryData_admissible line 277