one_lt_dist_of_ne_of_not_adj — Mathlib

English

If there is a path between u and v, u ≠ v, and u and v are not adjacent, then dist_G(u,v) > 1.

Русский

Если существует путь между u и v, u ≠ v и u, v не смежны, то dist_G(u,v) > 1.

LaTeX

$$$$ G.\mathrm{Reachable}(u,v) \land u \neq v \land \neg G.\mathrm{Adj}(u,v) \Rightarrow 1 < \mathrm{dist}_G(u,v) $$$$

Lean4

protected theorem one_lt_dist_of_ne_of_not_adj (h : G.Reachable u v) (hne : u ≠ v) (hnadj : ¬G.Adj u v) :
    1 < G.dist u v :=
  Nat.lt_of_le_of_ne (h.pos_dist_of_ne hne)
    (by
      by_contra! hc
      obtain ⟨p, hp⟩ := Reachable.exists_walk_length_eq_dist h
      exact hnadj (Walk.exists_length_eq_one_iff.mp ⟨p, hc ▸ hp⟩))

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