OAI/Analysis/CircleDomains/Selection/LocalPlateauContour.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local plateau admits a sufficiently deep genuine end contour that also avoids the fixed compact target anchor.

  1. theorem OAI.CircleDomainRigidity.FiniteTransfer.RealTargetEnd.exists_plateau_contour_avoiding_anchor line 20