OAI/GroupTheory/PolycyclicRecognition/Analysis/SelfQuasiIsometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform coarse inverse bounds for self quasi-isometries

  1. structure OAI.PolycyclicRecognition.SelfQuasiIsometry line 15

    Source documentation

    The usual upper, lower and coarse-surjectivity inequalities, with the lower inequality multiplied by K to avoid division. For 1 ≤ K this is exactly the standard (K,C) definition.

    Distinct definitions of this name: ComparatorChallenges/PolycyclicRecognition.lean:202 (different declaration text). Qualify references as OAI.PolycyclicRecognition.SelfQuasiIsometry@path.

    structure SelfQuasiIsometry where
…
  2. def OAI.PolycyclicRecognition.SelfQuasiIsometry.inverse line 23
  3. theorem OAI.PolycyclicRecognition.SelfQuasiIsometry.inverse_close line 26
  4. theorem OAI.PolycyclicRecognition.SelfQuasiIsometry.left_inverse_close line 30
  5. theorem OAI.PolycyclicRecognition.SelfQuasiIsometry.inverse_upper line 37