OAI/Analysis/CircleDomains/Modulus/SelectableLevelBarrier.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The small real-barrier alternative supplies an actual selectable coordinate compatible with every previously selected real or period coordinate. Its flags and presentation are constructed from the barrier.

  1. theorem OAI.CircleDomainRigidity.exists_selectable_level_barrier line 19