English
Non-adjacency is transitive in a Turán-maximal graph: if t is not adjacent to s and s is not adjacent to u, then t is not adjacent to u.
Русский
Не-смежность транспитивна: если t не смежен с s и s не смежен с u, то t не смежен с u.
LaTeX
$$$G.\mathrm{IsTuranMaximal } r \rightarrow (\neg G.Adj t s) \rightarrow (\neg G.Adj s u) \rightarrow (\neg G.Adj t u).$$$
Lean4
/-- In a Turán-maximal graph, non-adjacency is transitive. -/
theorem not_adj_trans (h : G.IsTuranMaximal r) (hts : ¬G.Adj t s) (hsu : ¬G.Adj s u) : ¬G.Adj t u :=
by
have hst : ¬G.Adj s t := fun a ↦ hts a.symm
have dst := h.degree_eq_of_not_adj hst
have dsu := h.degree_eq_of_not_adj hsu
rw [IsTuranMaximal] at h; contrapose! h; intro cf
classical
use (G.replaceVertex s t).replaceVertex s u, inferInstance, (cf.replaceVertex s t).replaceVertex s u
have nst : s ≠ t := fun a ↦ hsu (a ▸ h)
have ntu : t ≠ u := G.ne_of_adj h
have := (G.adj_replaceVertex_iff_of_ne s nst ntu.symm).not.mpr hsu
rw [card_edgeFinset_replaceVertex_of_not_adj _ this, card_edgeFinset_replaceVertex_of_not_adj _ hst, dst,
Nat.add_sub_cancel]
have l1 : (G.replaceVertex s t).degree s = G.degree s :=
by
unfold degree; congr 1; ext v
simp only [mem_neighborFinset]
by_cases eq : v = t
· simpa only [eq, not_adj_replaceVertex_same, false_iff]
· rw [G.adj_replaceVertex_iff_of_ne s nst eq]
have l2 : (G.replaceVertex s t).degree u = G.degree u - 1 :=
by
rw [degree, degree, ← card_singleton t, ← card_sdiff_of_subset (by simp [h.symm])]
congr 1; ext v
simp only [mem_neighborFinset, mem_sdiff, mem_singleton, replaceVertex]
split_ifs <;> simp_all [adj_comm]
have l3 : 0 < G.degree u := by rw [G.degree_pos_iff_exists_adj u]; use t, h.symm
cutsat
