OAI/Analysis/CircleDomains/Transfer/VerticalRetainedCrossings.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Retained target contours give crossing segments in the vertical direction.

  1. theorem OAI.CircleDomainRigidity.eventually_vertical_crossings_of_anchored_jordan_limits line 14
  2. theorem OAI.CircleDomainRigidity.eventually_vertical_crossings_of_retained_test line 53