OAI/Analysis/CircleDomains/Selection/SaturatedNonseparation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A closed union of whole complementary components of a connected open set is nonseparating. This allows clopen pieces of the compact obstacle to be handled together in finite shrinking stages.

  1. lemma OAI.CircleDomainRigidity.nonseparating_closed_saturated_complement line 11
  2. lemma OAI.CircleDomainRigidity.saturated_of_closed_relative_piece line 63
  3. lemma OAI.CircleDomainRigidity.nonseparating_closed_relative_complement_piece line 80