OAI/Geometry/Cannon/PlaneTopology/RadialStable.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonEmbeddedArc.Arc.slit_discrete_labels_constant line 56
  2. theorem OAI.CannonEmbeddedArc.Arc.tame_slit_connected line 95
  3. theorem OAI.CannonPolygonal.polyJoined_of_preconnected_finite_segments line 123
  4. theorem OAI.CannonPolygonal.preconnected_finite_segments_arc line 175
  5. theorem OAI.CannonEmbeddedArc.Arc.connected_graph_crosscut line 187
  6. def OAI.CannonSegmentCones.RadialStable line 227
  7. lemma OAI.CannonSegmentCones.radial_dist line 231
  8. lemma OAI.CannonSegmentCones.radial_mem_ball line 235
  9. lemma OAI.CannonSegmentCones.segment_split line 240
  10. lemma OAI.CannonSegmentCones.anchored_radial_stable line 260
  11. lemma OAI.CannonSegmentCones.RadialStable.mono_radius line 297
  12. lemma OAI.CannonSegmentCones.RadialStable.union line 301
  13. lemma OAI.CannonSegmentCones.segment_closed line 309
  14. lemma OAI.CannonSegmentCones.segment_radial_stable line 313
  15. theorem OAI.CannonSegmentCones.finite_segments_radial_stable line 328
  16. theorem OAI.CannonSegmentCones.component_radial_access line 339
  17. theorem OAI.CannonEmbeddedArc.Arc.finite_graph_exact_segments line 367
  18. lemma OAI.CannonEmbeddedArc.Arc.halfopen_radial_segment line 396
  19. theorem OAI.CannonEmbeddedArc.Arc.arc_to_accessible_point line 405
  20. theorem OAI.CannonEmbeddedArc.Arc.tame_component_accessible line 426
  21. lemma OAI.CannonSegmentCones.complex_segment_supporting_line line 447
  22. lemma OAI.CannonSegmentCones.complex_finite_segments_compl_dense line 469
  23. theorem OAI.CannonSegmentCones.refined_component_at_boundary line 494
  24. theorem OAI.CannonEmbeddedArc.Arc.arc_between_accessible_points line 540
  25. theorem OAI.CannonEmbeddedArc.Arc.finite_segment_component_crosscut line 566