OAI/Analysis/CircleDomains/Uniformization/ConformalComposition.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Composition in the concrete sphere charts

The finite and infinite charts are locally inverse at their centers. The ordinary complex chain rule therefore proves composition of the actual conformal-equivalence predicate used by the main statements.

  1. def OAI.CircleDomainRigidity.chartTransform line 21
  2. theorem OAI.CircleDomainRigidity.chartTransform_involutive line 24
  3. theorem OAI.CircleDomainRigidity.chart_eq_coordinate_transform line 32
  4. theorem OAI.CircleDomainRigidity.chartSymm_eq_transform line 37
  5. theorem OAI.CircleDomainRigidity.chartTransform_center_ne_infty line 42
  6. theorem OAI.CircleDomainRigidity.chartSymm_chart_of_ne line 51
  7. theorem OAI.CircleDomainRigidity.chartSymm_chart_self line 56
  8. theorem OAI.CircleDomainRigidity.continuous_chartSymm line 59
  9. theorem OAI.CircleDomainRigidity.eventually_chartSymm_chart line 65
  10. theorem OAI.CircleDomainRigidity.IsConformalAt.comp line 72
  11. theorem OAI.CircleDomainRigidity.IsConformalOn.comp line 96
  12. theorem OAI.CircleDomainRigidity.IsConformalEquivalence.trans line 101
  13. theorem OAI.CircleDomainRigidity.IsConformalEquivalence.symm_exists line 114
  14. theorem OAI.CircleDomainRigidity.IsConformalEquivalence.bijOn line 120