OAI/Analysis/CircleDomains/Topology/FiniteJordanModelInput.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CircleDomainRigidity.FiniteJordanModelUniformization line 11

   Source documentation

   Only the finite Jordan models, including their actual sphere chart changes, are needed by the downstream construction.

   def FiniteJordanModelUniformization : Prop :=
   …

2. lemma OAI.CircleDomainRigidity.finiteCircleUniformization_jordanModels line 17
3. lemma OAI.CircleDomainRigidity.FiniteTransfer.uniformize_finite_completion_of_jordan_models line 27