English
If p is a shortest walk from v to w of length dist(v,w) with dist(v,w) > 1, then there exist vertices x,a,b such that x∼a, a∼b, x not ∼ b, and x ≠ b.
Русский
Если p — кратчайший путь от v до w длиной dist(v,w) и dist(v,w) > 1, то существуют вершины x,a,b такие, что x~a, a~b, x не смежно с b, и x ≠ b.
LaTeX
$$$ \exists x,a,b \in V,\ G.Adj(x,a) \land G.Adj(a,b) \land \neg G.Adj(x,b) \land x \neq b$ (при условии, что p.length = dist(v,w) и 1 < dist(v,w))$$
Lean4
/-- This bundles and abstracts some facts about the first three vertices of a shortest walk
of length at least two: the first and third nodes are different and not connected. -/
theorem exists_adj_adj_not_adj_ne {p : G.Walk v w} (hp : p.length = G.dist v w) (hl : 1 < G.dist v w) :
∃ (x a b : V), G.Adj x a ∧ G.Adj a b ∧ ¬G.Adj x b ∧ x ≠ b :=
by
use v, p.getVert 1, p.getVert 2
have hnp : ¬p.Nil := by simpa [nil_iff_length_eq, hp] using Nat.ne_zero_of_lt hl
have : p.tail.tail.length < p.tail.length :=
by
rw [←
p.tail.length_tail_add_one
(by
simp only [not_nil_iff_lt_length, ← p.length_tail_add_one hnp] at hp ⊢
cutsat)]
omega
have : p.tail.length < p.length := by rw [← p.length_tail_add_one hnp]; omega
by_cases hv : v = p.getVert 2
· have : G.dist v w ≤ p.tail.tail.length := by simpa [hv, p.getVert_tail] using dist_le p.tail.tail
cutsat
by_cases hadj : G.Adj v (p.getVert 2)
· have : G.dist v w ≤ p.tail.tail.length + 1 := dist_le <| p.tail.tail.cons <| p.getVert_tail ▸ hadj
cutsat
exact ⟨p.adj_snd hnp, p.adj_getVert_succ (hp ▸ hl), hadj, hv⟩
