edist_triangle — Mathlib

English

If edist u v equals a natural k, there exists a walk p with length k.

Русский

Если edist u v равен натуральному числу k, существует путь длиной k.

LaTeX

$$$ \exists k : \mathbb{N}, G.edist u v = k \Rightarrow \exists p : G.Walk u v, p.length = k $$$

Lean4

protected theorem edist_triangle : G.edist u w ≤ G.edist u v + G.edist v w := by
  cases eq_or_ne (G.edist u v) ⊤ with
  | inl huv => simp [huv]
  | inr huv =>
    cases eq_or_ne (G.edist v w) ⊤ with
    | inl hvw => simp [hvw]
    | inr hvw =>
      obtain ⟨p, hp⟩ := exists_walk_of_edist_ne_top huv
      obtain ⟨q, hq⟩ := exists_walk_of_edist_ne_top hvw
      rw [← hp, ← hq, ← Nat.cast_add, ← Walk.length_append]
      exact edist_le _

Похожие утверждения