OAI/Analysis/CircleDomains/Selection/RestrictedMeanExclusion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Restricting to the common countable marks preserves a mean exclusion. Its source budget can only decrease, so the original open neighborhood remains excluded by a mixed limit retaining that coordinate.

  1. def OAI.CircleDomainRigidity.MeanExclusionWitness.restrictMarks line 20
  2. theorem OAI.CircleDomainRigidity.MeanExclusionWitness.neighborhood_subset_restrictMarks line 34
  3. theorem OAI.CircleDomainRigidity.MeanExclusionWitness.not_mem_neighborhood line 40