OAI/Geometry/Cannon/Boundary/BoundaryHomeomorph.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonRelease.translated_relation_closed line 26
  2. lemma OAI.CannonRelease.boundaryTranslate_graph_closed line 56
  3. lemma OAI.CannonRelease.boundaryTranslate_continuous line 83
  4. def OAI.CannonRelease.boundaryHomeomorph line 101
  5. def OAI.CannonRelease.boundaryAction line 111
  6. def OAI.CannonGraph.product2 line 126
  7. lemma OAI.CannonGraph.product2_add_dist line 128
  8. lemma OAI.CannonGraph.product2_le_twice_left line 134
  9. lemma OAI.CannonGraph.product2_comm line 140
  10. lemma OAI.CannonGraph.product2_le_twice_right line 143
  11. theorem OAI.CannonGraph.product2_hyperbolic line 148
  12. lemma OAI.CannonGraph.product2_ray_mono line 187
  13. abbrev OAI.CannonVisual.Ray line 216
  14. def OAI.CannonVisual.decay line 219
  15. def OAI.CannonVisual.preDist line 222
  16. lemma OAI.CannonVisual.preDist_le_decay line 224
  17. lemma OAI.CannonVisual.decay_comm line 227
  18. lemma OAI.CannonVisual.preDist_comm line 232
  19. lemma OAI.CannonVisual.decay_antitone line 235
  20. lemma OAI.CannonVisual.product2_self line 247
  21. lemma OAI.CannonVisual.preDist_self line 254
  22. lemma OAI.CannonVisual.exp_neg_mul_min line 279
  23. lemma OAI.CannonVisual.product2_four line 287
  24. lemma OAI.CannonVisual.decay_four line 296
  25. lemma OAI.CannonVisual.tendsto_decay line 313
  26. lemma OAI.CannonVisual.preDist_four line 317
  27. def OAI.CannonVisual.visualExponent line 326
  28. lemma OAI.CannonVisual.visualExponent_pos line 328
  29. lemma OAI.CannonVisual.visualExponent_small line 333
  30. def OAI.CannonVisual.rayPseudoMetric line 338
  31. lemma OAI.CannonVisual.visual_distance_le line 342
  32. lemma OAI.CannonVisual.preDist_le_twice_visual_distance line 346
  33. lemma OAI.CannonVisual.product2_ray_sum line 360
  34. lemma OAI.CannonVisual.product2_le_of_separated line 368
  35. lemma OAI.CannonVisual.preDist_pos_of_separated line 400
  36. lemma OAI.CannonVisual.tendsto_exp_linear line 411
  37. lemma OAI.CannonVisual.preDist_zero_of_bounded line 418
  38. theorem OAI.CannonVisual.preDist_zero_iff_bounded line 439
  39. theorem OAI.CannonVisual.visual_distance_zero_iff_bounded line 451
  40. def OAI.CannonVisual.raySetoid line 475
  41. def OAI.CannonVisual.MetricBoundary line 487
  42. def OAI.CannonVisual.boundaryDist line 489
  43. def OAI.CannonVisual.boundaryMetricSpace line 501
  44. lemma OAI.CannonVisual.boundary_dist_mk line 526
  45. lemma OAI.CannonVisual.decay_of_agree line 538
  46. lemma OAI.CannonVisual.continuous_boundary_mk line 545
  47. def OAI.CannonVisual.quotientVisualHomeomorph line 566
  48. def OAI.CannonRelease.visualMetricSpace line 589
  49. lemma OAI.CannonRelease.visualMetric_dist_ray line 597
  50. lemma OAI.CannonRelease.visualMetric_comparison line 601
  51. lemma OAI.CannonRelease.translateRay_uniform line 619
  52. lemma OAI.CannonRelease.translated_product2_bound line 630
  53. lemma OAI.CannonRelease.translated_preDist_le line 649
  54. lemma OAI.CannonRelease.boundaryTranslate_lipschitz_bound line 674