OAI/Analysis/CircleDomains/Selection/GradedRealSelection.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Countable selection of the constructed ungated tests, at every reciprocal accuracy. Compatibility retains every earlier test and its exceptional set.

  1. structure OAI.CircleDomainRigidity.GradedRealTest line 19
  2. def OAI.CircleDomainRigidity.GradedRealTest.Allowed line 27
  3. theorem OAI.CircleDomainRigidity.GradedRealTest.Allowed.mono line 31
  4. theorem OAI.CircleDomainRigidity.GradedRealTest.exists_countable_selection line 35
  5. theorem OAI.CircleDomainRigidity.GradedRealTest.exists_delayed_countable_selection line 49