OAI/Topology/ArtinGroups/ParabolicIntersections/GraphRealizationAction.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

An action on a graph extends isometrically to its unit-interval realization.

  1. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.actDart line 13
  2. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.actDart_injective line 15
  3. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.actPoint line 22
  4. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.actPoint_one line 26
  5. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.actPoint_mul line 35
  6. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.anchor_act line 46
  7. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.weight_act line 50
  8. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.route_act line 54
  9. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.distance_act line 58
  10. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.act line 74
  11. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.act_embed line 78
  12. def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.action line 87
  13. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.action_isometric line 98
  14. lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.act_vertex line 109