OAI/Analysis/CircleDomains/Modulus/LevelBarrierOpenExclusion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Apply the open real-barrier exclusion to the actual compatible barrier. Its compact omitted source set is constructed as the inverse image of the closed quotient penalty.

  1. theorem OAI.CircleDomainRigidity.CompatibleLevelBarrier.exists_open_exclusion line 19