OAI/Geometry/CylinderCovering/Radial/Triangle.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CylinderCovering.RadialTriangle.mem_region_iff line 10
2. lemma OAI.CylinderCovering.RadialTriangle.region_convex line 17
3. lemma OAI.CylinderCovering.RadialTriangle.vertices_mem_region line 31
4. lemma OAI.CylinderCovering.RadialTriangle.region_eq_convexHull line 37
5. lemma OAI.CylinderCovering.RadialTriangle.region_compact line 67
6. lemma OAI.CylinderCovering.RadialTriangle.vertices_affineIndependent line 72
7. lemma OAI.CylinderCovering.RadialTriangle.closed_region_volume line 88
8. lemma OAI.CylinderCovering.RadialTriangle.region_volume line 102
9. lemma OAI.CylinderCovering.RadialTriangle.region_volume_toReal line 131
10. lemma OAI.CylinderCovering.RadialTriangle.vertices_det line 136
11. lemma OAI.CylinderCovering.RadialTriangle.region_measurable line 144
12. lemma OAI.CylinderCovering.RadialTriangle.region_volume_ne_top line 147
13. lemma OAI.CylinderCovering.RadialTriangle.freezing_left_lt_right line 152
14. lemma OAI.CylinderCovering.RadialTriangle.freezingRegion_volume line 160
15. lemma OAI.CylinderCovering.RadialTriangle.region_image_eq_convexHull line 172
16. lemma OAI.CylinderCovering.RadialTriangle.image_vertices_affineIndependent line 177