OAI/Analysis/CircleDomains/Reflection/ConformalBoundaryChart.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Apply the constructed modulus continuation to an actual conformal map in a holomorphic boundary chart. No boundary values of the conformal map are assumed.

  1. lemma OAI.CircleDomainRigidity.conformal_disk_boundary_chart_data line 15
  2. lemma OAI.CircleDomainRigidity.conformal_disk_boundary_chart_continuation line 58