OAI/Analysis/CircleDomains/Topology/RegularJordanSideChoice.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The choice of the inward scalar-level side is consistent along a connected Jordan boundary.

  1. lemma OAI.CircleDomainRigidity.regular_jordan_side_incompatible line 12
  2. lemma OAI.CircleDomainRigidity.regular_jordan_global_side line 46