MetricUnitCurves.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Concatenation of unit-speed curves and realization of distance.

def OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.HasCurve line 10
lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_const line 13
lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_subsegment line 16
lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_reverse line 33
lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_concat line 40
lemma OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.curve_realizes_distance line 76
Source documentation
A unit-speed curve whose length is the endpoint distance is a geodesic.
```
lemma curve_realizes_distance {x y : X} (hc : HasCurve x y (dist x y)) :
    ∃ γ : Set.Icc (0 : ℝ) (dist x y) → X, Isometry γ ∧
      γ ⟨0,le_rfl,dist_nonneg⟩=x ∧ γ ⟨dist x y,dist_nonneg,le_rfl⟩=y := by
…
```
Mentions: OAI.HarmonicArtin.ParabolicIntersections.GraphRealization.HasCurve