OAI/Analysis/CircleDomains/Uniformization/UniformLimitFibers.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Exact fiber identities and surjectivity for limits of homeomorphisms.

  1. lemma OAI.CircleDomainRigidity.surjective_uniform_limit line 12
  2. lemma OAI.CircleDomainRigidity.uniform_limit_inverse_observation line 27
  3. lemma OAI.CircleDomainRigidity.uniform_limit_eq_of_shrinking_distance line 40