exists_walk_of_edist_eq_coe — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem exists_walk_of_edist_eq_coe {k : ℕ} (h : G.edist u v = k) : ∃ p : G.Walk u v, p.length = k :=
  have : G.edist u v ≠ ⊤ := by rw [h]; exact ENat.coe_ne_top _
  have ⟨p, hp⟩ := exists_walk_of_edist_ne_top this
  ⟨p, Nat.cast_injective (hp.trans h)⟩

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