OAI/Analysis/CircleDomains/Reflection/InjectiveConformalBoundaryChart.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual conformal equivalence, in an injective source chart, has an injective holomorphic continuation with nonzero boundary derivative.

  1. lemma OAI.CircleDomainRigidity.injective_conformal_disk_boundary_chart_sides line 14
  2. lemma OAI.CircleDomainRigidity.injective_conformal_disk_boundary_chart line 40
  3. lemma OAI.CircleDomainRigidity.injective_circular_exterior_boundary_chart_sides line 57
  4. lemma OAI.CircleDomainRigidity.injective_circular_exterior_boundary_chart line 73