OAI/Analysis/CircleDomains/Modulus/FixedNormalOrientation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One sign works in every local boundary chart of the same Jordan circuit, before any differential form is chosen.

  1. lemma OAI.CircleDomainRigidity.normal_box_sides_fixed line 13
  2. lemma OAI.CircleDomainRigidity.regular_jordan_local_green_sign line 51