OAI/Analysis/CircleDomains/Topology/CellularJordanNeighborhood.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A nonempty compact nonseparating plane continuum has arbitrarily small Jordan-disk neighborhoods. The finite contour cover reduces to one disk by connectedness; no sphere-decomposition theorem is used.

  1. lemma OAI.CircleDomainRigidity.connected_subset_one_of_disjoint_open_cover line 12
  2. lemma OAI.CircleDomainRigidity.exists_jordan_neighborhood_of_nonseparating_continuum line 36