OAI/Analysis/CircleDomains/Topology/ComponentQuotientNoCutPoint.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The constructed component quotient has no cut points. Nonseparation is proved on the source sphere and passes through the actual quotient.

  1. lemma OAI.CircleDomainRigidity.sphere_compl_singleton_connected line 12
  2. lemma OAI.CircleDomainRigidity.componentProjection_fiber_complement_connected line 28
  3. lemma OAI.CircleDomainRigidity.componentQuotient_no_cut_points line 62