OAI/Geometry/CylinderCovering/Cartesian/Domain.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.CartesianCaps.height_lower line 11
2. lemma OAI.CylinderCovering.CartesianCaps.height_upper line 16
3. lemma OAI.CylinderCovering.CartesianCaps.height_le_three_quarters line 22
4. lemma OAI.CylinderCovering.CartesianCaps.central_subset_domain line 28
5. lemma OAI.CylinderCovering.CartesianCaps.domain_enclosure line 35
6. lemma OAI.CylinderCovering.CartesianCaps.integral_D line 54
7. lemma OAI.CylinderCovering.CartesianCaps.integral_abs_half line 62
8. lemma OAI.CylinderCovering.CartesianCaps.integral_height line 79
9. lemma OAI.CylinderCovering.CartesianCaps.volume_central line 90
10. lemma OAI.CylinderCovering.CartesianCaps.volume_rectangle line 104
11. theorem OAI.CylinderCovering.CartesianCaps.domain_area_bounds line 111
12. lemma OAI.CylinderCovering.CartesianCaps.domain_isClosed line 158
13. lemma OAI.CylinderCovering.CartesianCaps.domain_isCompact line 168
14. lemma OAI.CylinderCovering.CartesianCaps.domain_radial line 174
15. theorem OAI.CylinderCovering.CartesianCaps.domain_area_expansion line 208
16. lemma OAI.CylinderCovering.CartesianCaps.untruncated_contains_ray line 215
17. lemma OAI.CylinderCovering.CartesianCaps.untruncated_not_bddAbove line 241
18. lemma OAI.CylinderCovering.CartesianCaps.untruncated_gap line 251