OAI/Analysis/CircleDomains/Selection/NearExtremalHeightCloseness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform compact-set closeness for the actual model heights, together with their zero gradient on the actual complement.

  1. theorem OAI.CircleDomainRigidity.uniform_near_extremal_height line 13