OAI/Analysis/CircleDomains/Topology/RegularJordanLevelComponent.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A Jordan boundary lying in a regular scalar level is an open compact connected component of that level, even if the rest of the level is unbounded.

  1. lemma OAI.CircleDomainRigidity.regular_jordan_boundary_open_in_level line 13