OAI/Analysis/CircleDomains/Topology/LevelChartJordanSides.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The two halves of an actual scalar-level chart lie on opposite sides of a Jordan boundary contained in that level.

  1. lemma OAI.CircleDomainRigidity.level_chart_jordan_sides line 13