OAI/Geometry/Cannon/ScalarLimits/Words.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CannonRelease.boundary_stabilizer_linear line 38
  2. def OAI.CannonStabilizer.words line 70
  3. lemma OAI.CannonStabilizer.words_preserve line 74
  4. lemma OAI.CannonStabilizer.words_card line 92
  5. lemma OAI.CannonStabilizer.words_mem line 121
  6. lemma OAI.CannonStabilizer.words_length line 139
  7. lemma OAI.CannonStabilizer.exists_exponential_gt_linear line 163
  8. theorem OAI.CannonStabilizer.no_disjoint_contractions line 173
  9. def OAI.CannonStabilizer.ContractingDirection line 189
  10. theorem OAI.CannonStabilizer.contracting_direction_unique line 194
  11. def OAI.CannonStabilizer.homAction line 238
  12. theorem OAI.CannonStabilizer.contracting_direction_of_fixed_puncture line 244
  13. theorem OAI.CannonStabilizer.puncture_fibers_finite line 318
  14. theorem OAI.CannonStabilizer.injective_subsequence_of_finite_fibers line 342
  15. def OAI.CannonVariation.NonconstantAt line 371
  16. theorem OAI.CannonVariation.path_meets_variation line 374
  17. lemma OAI.CannonVariation.nonconstantAt_normalize line 387
  18. theorem OAI.CannonVariation.value_subpath line 392