OAI/Geometry/Cannon/PlaneTopology/FaceVerticesCard.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CannonEmbeddedArc.Arc.face_vertices_card_le line 55
2. lemma OAI.CannonEmbeddedArc.Arc.stellar_old_edge_parent line 86
3. theorem OAI.CannonEmbeddedArc.Arc.stellar_face_edges_card_le line 94
4. lemma OAI.CannonEmbeddedArc.Arc.stellar_spoke_closure line 133
5. theorem OAI.CannonEmbeddedArc.Arc.near_faces_card_le line 146
6. theorem OAI.CannonEmbeddedArc.Arc.stellar_spokes_local_card line 179
7. theorem OAI.CannonEmbeddedArc.Arc.stellar_graph_local_card line 222
8. theorem OAI.CannonEmbeddedArc.Arc.vertices_local_card line 250
9. lemma OAI.CannonEmbeddedArc.Arc.support_subset_stellar line 278
10. lemma OAI.CannonEmbeddedArc.Arc.stellar_support_finite line 286
11. lemma OAI.CannonEmbeddedArc.Arc.stellar_faces_diam line 299
12. theorem OAI.CannonEmbeddedArc.Arc.quantitative_triangular_refinement line 307
13. lemma OAI.CannonEmbeddedArc.Arc.continuous_closure_diam line 381