OAI/Topology/ArtinGroups/ParabolicIntersections/GraphRealizationGeodesic.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Shortest paths in the unit-interval realization of a connected graph.

  1. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.arc_curve line 11
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_to_anchor line 24
  3. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_of_adj line 37
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_of_walk line 43
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_between_vertices line 52
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_via line 57
  7. theorem OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_between line 65
  8. theorem OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.realization_geodesic line 75