OAI/Analysis/CircleDomains/Topology/VerticalFrontierCrossings.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Crossing segments from nested bounded regions

On any vertical line meeting the inner region, the bottommost points of the inner and outer closures lie on their frontiers. Strict containment puts the outer point strictly below. Thus prescribed zero/one frontier values provide the crossing segments needed by line payment.

  1. theorem OAI.CircleDomainRigidity.continuous_verticalLine line 22
  2. theorem OAI.CircleDomainRigidity.exists_bottommost_vertical_frontier line 25
  3. theorem OAI.CircleDomainRigidity.exists_vertical_frontier_crossing line 62
  4. theorem OAI.CircleDomainRigidity.vertical_frontier_crossings_give_values line 81