OAI/Analysis/CircleDomains/Selection/RealExclusionWitness.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A real barrier test retains its actual presentation, band weight, open map neighborhood, and the proved radius-dependent exclusion.

  1. structure OAI.CircleDomainRigidity.RealExclusionWitness line 19
  2. def OAI.CircleDomainRigidity.RealExclusionWitness.sizedNeighborhood line 47
  3. theorem OAI.CircleDomainRigidity.RealExclusionWitness.isOpen_sizedNeighborhood line 50
  4. theorem OAI.CircleDomainRigidity.RealExclusionWitness.mem_sizedNeighborhood line 53
  5. theorem OAI.CircleDomainRigidity.SelectedMixedModels.excludes_retained_sized_real line 69