exists_length_eq_one_iff — Mathlib

English

There exists a walk of length 1 between u and v if and only if u and v are adjacent.

Русский

Существует путь длины 1 между u и v тогда и только тогда, когда u и v смежны.

LaTeX

$$$(\exists p: G.Walk u v, \operatorname{length}(p) = 1) \iff G.Adj u v$$$

Lean4

@[simp]
theorem exists_length_eq_one_iff {u v : V} : (∃ (p : G.Walk u v), p.length = 1) ↔ G.Adj u v :=
  by
  refine ⟨?_, fun h ↦ ⟨h.toWalk, by simp⟩⟩
  rintro ⟨p, hp⟩
  induction p with
  | nil => simp only [Walk.length_nil, zero_ne_one] at hp
  | cons h p' =>
    simp only [Walk.length_cons, add_eq_right] at hp
    exact (p'.eq_of_length_eq_zero hp) ▸ h

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