OAI/Geometry/Cannon/PlaneTopology/PairComponentClosure.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonEmbeddedArc.Arc.pair_component_closure line 53
2. theorem OAI.CannonEmbeddedArc.Arc.isolated_jordan_face line 78
3. lemma OAI.CannonEmbeddedArc.Arc.walk_edge_mem line 156
4. lemma OAI.CannonEmbeddedArc.Arc.walkCarrier_edgeUnion line 165
5. theorem OAI.CannonEmbeddedArc.Arc.facial_jordan_cycle line 172
6. lemma OAI.CannonEmbeddedArc.Arc.facial_boundary_preconnected line 235
7. lemma OAI.CannonEmbeddedArc.Arc.third_facial_edge_impossible line 245
8. theorem OAI.CannonEmbeddedArc.Arc.triangle_whole_face line 261
9. theorem OAI.CannonEmbeddedArc.Arc.refined_face_new_edge line 335
10. lemma OAI.CannonEmbeddedArc.Arc.face_local_access line 384
11. lemma OAI.CannonEmbeddedArc.Arc.arc_endpoint_closure_interior line 401
12. theorem OAI.CannonEmbeddedArc.Arc.spoke_forces_new_facial_edge line 406
13. lemma OAI.CannonEmbeddedArc.Arc.face_parent line 427
14. lemma OAI.CannonEmbeddedArc.Arc.same_face_of_mem_closure line 439
15. lemma OAI.CannonEmbeddedArc.Arc.stellar_spoke_parent line 448
16. lemma OAI.CannonEmbeddedArc.Arc.stellar_old_endpoint line 467
17. theorem OAI.CannonEmbeddedArc.Arc.stellar_old_vertex_spoke_facial line 479
18. lemma OAI.CannonEmbeddedArc.Arc.stellar_face_old_edge line 503
19. theorem OAI.CannonEmbeddedArc.Arc.stellar_face_triangle line 538
20. theorem OAI.CannonEmbeddedArc.Arc.global_triangular_stellation line 611