OAI/Geometry/Cannon/PlaneTopology/ClosedInside.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonTriangleWinding.area_combo line 16
2. def OAI.CannonTriangleWinding.ClosedInside line 23
3. lemma OAI.CannonTriangleWinding.closedInside_convex line 24
4. lemma OAI.CannonTriangleWinding.area_barycentric line 31
5. lemma OAI.CannonTriangleWinding.convexHull_eq_closedInside line 41
6. lemma OAI.CannonTriangleWinding.convexHull_interior_nonempty line 72
7. lemma OAI.CannonTriangleWinding.area_isOpenMap line 92
8. lemma OAI.CannonTriangleWinding.area_continuous line 106
9. lemma OAI.CannonTriangleWinding.convexHull_interior line 110
10. lemma OAI.CannonTriangleWinding.convexHull_closure_inside line 124
11. lemma OAI.CannonTriangleWinding.segment_subset_frontier line 135
12. lemma OAI.CannonTriangleWinding.vertices_segment_frontier line 149
13. lemma OAI.CannonEmbeddedArc.Arc.FacialCycle.hull_eq line 181
14. lemma OAI.CannonEmbeddedArc.Arc.graph_extension_frontier line 188
15. theorem OAI.CannonEmbeddedArc.Arc.exists_spherical_facewise_realization line 224
16. theorem OAI.CannonEmbeddedArc.Arc.DevelopedFaces.spherical_realization line 335
17. theorem OAI.CannonEmbeddedArc.Arc.exists_facewise_surjective_realization line 387
18. lemma OAI.CannonEmbeddedArc.Arc.FacialCycle.hull_radius_bound line 457
19. lemma OAI.CannonEmbeddedArc.Arc.facial_star_image_bound line 478