OAI/Analysis/CircleDomains/Selection/ControlledHeightCloseness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The height tolerance is uniform over all retained models with one fixed exterior radius. Only the near-extremality error must shrink.

  1. theorem OAI.CircleDomainRigidity.controlled_heights_close line 12