exists_length_eq_zero_iff — Mathlib

English

There exists a zero-length walk from u to v if and only if u = v.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem exists_length_eq_zero_iff {u v : V} : (∃ p : G.Walk u v, p.length = 0) ↔ u = v :=
  by
  constructor
  · rintro ⟨p, hp⟩
    exact eq_of_length_eq_zero hp
  · rintro rfl
    exact ⟨nil, rfl⟩

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