OAI/Analysis/CircleDomains/Selection/NearMaximalHeightSelection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Select an actual nearly maximal model and its actual controlled height, with prescribed compact closeness and a prescribed small deficit.

  1. theorem OAI.CircleDomainRigidity.exists_close_model_height line 13