one_lt_dist_of_ne_of_not_adj — Mathlib

English

If G is connected, u ≠ v, and u and v are not adjacent, then dist_G(u,v) > 1.

Русский

Если граф G связный, u ≠ v, и u и v не смежны, тогда dist_G(u,v) > 1.

LaTeX

$$$$ G.Connected \Rightarrow (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.Connected) (hne : u ≠ v) (hnadj : ¬G.Adj u v) : 1 < G.dist u v :=
  Reachable.one_lt_dist_of_ne_of_not_adj (h u v) hne hnadj

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