OAI/Analysis/CircleDomains/Modulus/NormalChartJordanSides.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two halves of a normal chart lie on the two different Jordan sides.

  1. lemma OAI.CircleDomainRigidity.normal_chart_jordan_sides line 12