OAI/Analysis/CircleDomains/Selection/CoordinateExclusionTest.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Real and mean tests use one common map--disk--radius space. The mark index is kept discrete, so each selected test retains the component it excludes.

  1. structure OAI.CircleDomainRigidity.MeanExclusionTest line 17
  2. structure OAI.CircleDomainRigidity.CoordinateExclusionTest line 31
  3. def OAI.CircleDomainRigidity.CoordinateExclusionTest.presentation line 43
  4. def OAI.CircleDomainRigidity.CoordinateExclusionTest.neighborhood line 46
  5. theorem OAI.CircleDomainRigidity.CoordinateExclusionTest.isOpen_neighborhood line 50
  6. theorem OAI.CircleDomainRigidity.CoordinateExclusionTest.excludes_retained line 58