OAI/Analysis/CircleDomains/Topology/JordanLocalSides.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two connected local sides of a Jordan boundary lie on opposite sides. The proof uses density and regular openness of the actual Jordan disk.

  1. lemma OAI.CircleDomainRigidity.connected_disjoint_jordan_boundary line 12
  2. lemma OAI.CircleDomainRigidity.jordan_local_sides line 26