OAI/Analysis/CircleDomains/Selection/AnnularOuterNonconstant.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Two distinct points in the exterior half of a symmetric circle collar.

  1. lemma OAI.CircleDomainRigidity.symmetricCircleAnnulus_outer_nontrivial line 10
  2. lemma OAI.CircleDomainRigidity.not_constant_of_injective_outer_annulus line 28