OAI/Analysis/CircleDomains/Selection/SizedMeanExclusion.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Record the exterior model radius in the same second countable test space. An open radius interval retains the quantitative Stokes exclusion under subsequent common-model selection.

  1. def OAI.CircleDomainRigidity.MeanExclusionWitness.sizedNeighborhood line 20
  2. theorem OAI.CircleDomainRigidity.MeanExclusionWitness.isOpen_sizedNeighborhood line 23
  3. theorem OAI.CircleDomainRigidity.MeanExclusionWitness.mem_sizedNeighborhood line 26
  4. theorem OAI.CircleDomainRigidity.MeanExclusionWitness.not_mem_sizedNeighborhood line 30