OAI/Analysis/CircleDomains/Selection/SelectedRadiusLowerBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform nondegeneration of the actual selected round holes.

  1. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.PhaseCollar.selectedRadius_lower_bound line 15
  2. lemma OAI.CircleDomainRigidity.FiniteJordanConfiguration.selectedRadii_common_lower_bound line 31