OAI/Topology/ArtinGroups/ParabolicIntersections/GraphRealizationSpace.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

The metric realization of a connected graph by unit intervals.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_vertices line 10
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_edge line 13
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.weight_le_one line 27
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_anchor_le line 32
  5. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.Space line 36
  6. instance OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.spaceMetric line 39
  7. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.embed line 42
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.dist_embed line 45
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.embed_surjective line 48
  10. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.vertex line 51
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.dist_vertex line 53
  12. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.vertex_injective line 56
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.exists_near_vertex line 61
  14. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.arc line 66
  15. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.dist_arc line 69
  16. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.arc_zero line 72
  17. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.arc_one line 78