OAI/Analysis/CircleDomains/Uniformization/LabelledCoreIteration.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual compact core maps preserve every boundary label under finite composition.

  1. def OAI.CircleDomainRigidity.FiniteJordanConfiguration.boundaryInCore line 15
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.boundaryInCore_image line 18
  3. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.Step.exists_labelled_core_equiv line 26
  4. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.exists_cumulative_labelled_core_equiv line 38