edgeFinset_sup_edge — Mathlib

English

If s and t are not adjacent (hn) and s ≠ t (h), then the edgeFinset of G ⊔ edge s t has cardinality one more than the edgeFinset of G.

Русский

Если s и t не смежны и s ≠ t, то число ребер в графе G ⊔ edge s t на единицу больше числа ребер в G.

LaTeX

$$$\\neg G.Adj\\ s\\ t \\to\\ s \\neq t \\to \\#\$G \\sqcup edge\\ s\\ t\$.edgeFinset = \\#G.edgeFinset + 1$$$

Lean4

theorem edgeFinset_sup_edge [Fintype (edgeSet (G ⊔ edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) :
    (G ⊔ edge s t).edgeFinset = G.edgeFinset.cons s(s, t) (by simp_all) :=
  by
  letI := Classical.decEq V
  rw [edgeFinset_sup, cons_eq_insert, insert_eq, union_comm]
  simp_rw [edgeFinset, edge_edgeSet_of_ne h]; rfl

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