OAI/Analysis/CircleDomains/Topology/ClosedRelationQuotient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Closed equivalence relations on compact Hausdorff spaces have closed quotient maps and Hausdorff quotient spaces. These elementary topological bridges precede the sphere realization in the Moore application.

  1. lemma OAI.CircleDomainRigidity.quotientMk_isClosedMap_of_closed_relation line 14
  2. lemma OAI.CircleDomainRigidity.quotientMk_fiber_isClosed_of_closed_relation line 31
  3. lemma OAI.CircleDomainRigidity.quotient_t2Space_of_closed_relation line 42