OAI/Analysis/CircleDomains/Topology/ConnectedExteriorNeighborhood.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact nonseparating plane sets admit arbitrarily small open neighborhoods with connected unbounded complements. The exterior is constructed by attaching finitely many compact paths and closed balls to an existing exterior.

  1. lemma OAI.CircleDomainRigidity.exists_closed_connected_enlargement line 14
  2. lemma OAI.CircleDomainRigidity.exists_open_connected_exterior_neighborhood line 59