OAI/Analysis/CircleDomains/Topology/ComponentQuotientModel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The topological quotient by complementary components has a compatible metric, an open domain chart, and a totally disconnected remainder. Moore's decomposition theorem realizes this quotient as a sphere.

  1. abbrev OAI.CircleDomainRigidity.ComponentQuotient line 15
  2. def OAI.CircleDomainRigidity.componentProjection line 17
  3. lemma OAI.CircleDomainRigidity.componentProjection_continuous line 19
  4. lemma OAI.CircleDomainRigidity.componentProjection_surjective line 22
  5. lemma OAI.CircleDomainRigidity.componentProjection_eq line 25
  6. lemma OAI.CircleDomainRigidity.componentProjection_closed line 29
  7. lemma OAI.CircleDomainRigidity.componentQuotient_t2 line 34
  8. lemma OAI.CircleDomainRigidity.componentQuotient_secondCountable line 38
  9. lemma OAI.CircleDomainRigidity.componentQuotient_metrizable line 49
  10. lemma OAI.CircleDomainRigidity.componentQuotient_locallyConnected line 55
  11. lemma OAI.CircleDomainRigidity.componentQuotient_domain_model line 64
  12. lemma OAI.CircleDomainRigidity.componentQuotient_connected_fibers line 76