OAI/Analysis/CircleDomains/Selection/LocalHeightFlattening.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual height admits simultaneous uniform and local energy flattening at the countably many selected end values.

  1. theorem OAI.CircleDomainRigidity.ControlledHeight.exists_local_value_flattening line 13