OAI/Analysis/CircleDomains/Modulus/RegularJordanNormalSides.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform local rectangles of the actual normal strip have one inward and one outward half; no orientation is assumed.

  1. def OAI.CircleDomainRigidity.NormalSidePattern line 13
  2. lemma OAI.CircleDomainRigidity.exists_local_normal_side_pattern line 22