OAI/Topology/ArtinGroups/ParabolicIntersections/GraphRealizationDistance.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

The path distance on unit intervals attached to graph edges.

  1. inductive OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.Point line 13

    Source documentation

    Endpoints are retained at this stage and identified by the metric quotient.

    inductive Point where
…
  2. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.anchor line 17
  3. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.weight line 22
  4. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.route line 27
  5. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.via line 30
  6. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance line 34
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.weight_nonneg line 39
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.route_nonneg line 44
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.via_le_route line 47
  10. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.via_eq_route line 50
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_le_via line 61
  12. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_le_route line 65
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_le_direct line 68
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_cases line 72
  15. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_nonneg line 89
  16. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.route_comm line 94
  17. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_comm line 99
  18. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_self line 108
  19. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.anchor_bridge line 114
  20. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.edge_weight_le line 124
  21. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.route_triangle line 130
  22. theorem OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_triangle line 142
  23. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.premetric line 174