OAI/Analysis/CircleDomains/Topology/CutPathComponents.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A closed-disk crosscut complement is locally path connected. Thus the connected sides already proved are its actual path components.

  1. theorem OAI.CircleDomainRigidity.HalfPlaneRay.cutDomain_locallyPathConnected line 15
  2. theorem OAI.CircleDomainRigidity.HalfPlaneRay.side_fiber_preconnected line 43
  3. theorem OAI.CircleDomainRigidity.HalfPlaneRay.side_eq_iff_joined line 83