OAI/Analysis/CircleDomains/Modulus/LevelBarrierSlackExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The constructed barrier excludes a whole open interval of model radii around the current one, as required by countable open selection.

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