OAI/Analysis/CircleDomains/Selection/SlackRealExclusion.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A strictly larger comparison radius gives an open radius interval in the countable selection space while retaining the same real barrier test.

  1. def OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.selectionRadius line 16
  2. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.model_lt_selectionRadius line 18
  3. def OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.selectionThreshold line 23
  4. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.selectionThreshold_pos line 26
  5. theorem OAI.CircleDomainRigidity.FiniteTransfer.LocalEndTestGeometry.exists_open_real_barrier_exclusion_at_radius line 31