OAI/Analysis/CircleDomains/Topology/HorizontalFrontierCrossings.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Crossing segments from nested bounded regions

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

  1. theorem OAI.CircleDomainRigidity.exists_leftmost_horizontal_frontier line 22
  2. theorem OAI.CircleDomainRigidity.exists_horizontal_frontier_crossing line 59
  3. theorem OAI.CircleDomainRigidity.horizontal_frontier_crossings_give_values line 78