OAI/Geometry/Cannon/PlaneTopology/FiniteSupport.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CannonEmbeddedArc.Arc.trans_injective line 25
2. theorem OAI.CannonEmbeddedArc.Arc.extend_arc line 52
3. def OAI.CannonPolygonal.FiniteSupport line 109
4. lemma OAI.CannonPolygonal.FiniteSupport.mono line 111
5. lemma OAI.CannonPolygonal.FiniteSupport.segment line 115
6. lemma OAI.CannonPolygonal.FiniteSupport.union line 118
7. def OAI.CannonPolygonal.PolyJoined line 131
8. lemma OAI.CannonPolygonal.polyJoined_of_open_preconnected line 134
9. theorem OAI.CannonPolygonal.polyJoined_arc line 163
10. theorem OAI.CannonPolygonal.open_preconnected_arc line 199
11. lemma OAI.CannonRegularDisk.IsRegularDisk.isPathConnected line 207
12. lemma OAI.CannonRegularDisk.IsRegularDisk.punctured_pathConnected line 212
13. theorem OAI.CannonPolygonal.regular_disk_chart_arc line 250