OAI/Analysis/CircleDomains/Topology/CountableJordanCollars.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A single countable family of genuine Jordan collars is a neighborhood basis at every finite dust point. Boundaries lie in the quotient domain.

  1. def OAI.CircleDomainRigidity.quotientJordanDisk line 19
  2. theorem OAI.CircleDomainRigidity.exists_countable_jordan_collars line 22