OAI/Analysis/CircleDomains/Topology/CrosscutBoundarySeparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A connected set in the closed disk avoiding a crosscut cannot join its two boundary arcs. This includes continua that run along the circle.

  1. lemma OAI.CircleDomainRigidity.crosscut_closed_side_locally_open line 13
  2. lemma OAI.CircleDomainRigidity.connected_avoiding_crosscut_one_side line 34