OAI/Analysis/CircleDomains/Selection/Nonseparation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Nonseparation of complementary components

Complementary components of a connected sphere domain do not separate the sphere, as required by Moore's 1925 decomposition theorem.

  1. theorem OAI.CircleDomainRigidity.isClosed_componentIn line 17
  2. theorem OAI.CircleDomainRigidity.nonseparating_complementaryComponent line 27

    Source documentation

    In a connected locally connected space, every complementary component of a nonempty connected open set is nonseparating.

    theorem nonseparating_complementaryComponent
    {X : Type*} [TopologicalSpace X] [PreconnectedSpace X] [LocallyConnectedSpace X]
    {G : Set X} (hopen : IsOpen G) (hconn : IsConnected G) {p : X} (hp : p ∉ G) :
    IsConnected (connectedComponentIn Gᶜ p)ᶜ := by
…