OAI/Geometry/Cannon/Boundary/Thin.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

Thin geodesic triangles and fellow travelling in the Cayley graph.

  1. def OAI.CannonGraph.Thin line 20
  2. lemma OAI.CannonGraph.start_getVert_dist line 25
  3. lemma OAI.CannonGraph.getVert_end_dist line 35
  4. lemma OAI.CannonGraph.getVert_dist_le line 44
  5. lemma OAI.CannonGraph.of_mem_geodesic line 50
  6. lemma OAI.CannonGraph.opposite_side_bound line 61
  7. lemma OAI.CannonGraph.synchronous_of_near line 71
  8. lemma OAI.CannonGraph.fellow_travel_below_product line 94
  9. theorem OAI.CannonGraph.synchronous_prefix line 111
  10. def OAI.CannonGraph.raySegment line 138
  11. lemma OAI.CannonGraph.raySegment_length line 143
  12. lemma OAI.CannonGraph.raySegment_getVert line 150
  13. theorem OAI.CannonGraph.asymptotic_rays_uniform line 168
  14. lemma OAI.CannonGraph.finite_short_walk_ends line 199
  15. lemma OAI.CannonGraph.finite_graph_ball line 217
  16. lemma OAI.CannonGraph.finite_cayley_neighbors line 224
  17. theorem OAI.CannonGraph.compact_ray_space line 233
  18. lemma OAI.CannonGraph.geodesic_getVert_dist line 262
  19. lemma OAI.CannonGraph.different_bases_same_endpoint line 278
  20. theorem OAI.CannonGraph.exists_rebased_ray line 319
  21. lemma OAI.CannonBoundary.quotient_closedMap line 377
  22. theorem OAI.CannonBoundary.quotient_t2_of_closed line 393
  23. def OAI.CannonRelease.CannonStatement line 432
  24. theorem OAI.CannonRelease.finite_kernel_of_proper line 438
  25. instance OAI.CannonRelease.basedRay_compactSpace line 456
  26. instance OAI.CannonRelease.boundary_compactSpace line 461
  27. lemma OAI.CannonRelease.raySetoid_isClosed line 464
  28. theorem OAI.CannonRelease.boundary_t2Space line 488
  29. lemma OAI.CannonGraph.iso_dist line 498
  30. theorem OAI.CannonGraph.asymptotic_rays_different_bases_uniform line 506
  31. def OAI.CannonRelease.CayleyData.leftIso line 536
  32. lemma OAI.CannonRelease.CayleyData.dist_mul_left line 541
  33. def OAI.CannonRelease.Asymptotic line 545
  34. lemma OAI.CannonRelease.Asymptotic.refl line 548
  35. lemma OAI.CannonRelease.Asymptotic.symm line 551
  36. lemma OAI.CannonRelease.Asymptotic.trans line 556
  37. lemma OAI.CannonRelease.Asymptotic.mul_left line 564
  38. lemma OAI.CannonRelease.exists_translate_ray line 572
  39. def OAI.CannonRelease.translateRay line 582
  40. lemma OAI.CannonRelease.translateRay_spec line 585
  41. lemma OAI.CannonRelease.translateRay_respects line 589
  42. def OAI.CannonRelease.boundaryTranslate line 597
  43. lemma OAI.CannonRelease.boundaryTranslate_mk line 602
  44. lemma OAI.CannonRelease.boundaryTranslate_one line 605
  45. lemma OAI.CannonRelease.boundaryTranslate_mul line 612