OAI/Analysis/CircleDomains/Modulus/SelectableBarrierExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual small compatible barrier supplies both its selectable coordinate and the open sized real exclusion carried into the final model.

  1. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.exists_selectable_exclusion line 17