card_edgeFinset_sup_edge — Mathlib

English

For not adjacent and distinct endpoints, the edgeFinset card increases by one when adding the edge between s and t.

Русский

При не смежности концов и их различности число рёбер увеличивается на единицу при добавлении ребра между s и t.

LaTeX

$$$\\neg G.Adj\\ s\\ t \\to \\ Ne\\ s\\ t \\to \\#(G \\sqcup edge\\ s\\ t).edgeFinset.card = \\#G.edgeFinset.card + 1$$$

Lean4

theorem card_edgeFinset_sup_edge [Fintype (edgeSet (G ⊔ edge s t))] (hn : ¬G.Adj s t) (h : s ≠ t) :
    #(G ⊔ edge s t).edgeFinset = #G.edgeFinset + 1 := by rw [G.edgeFinset_sup_edge hn h, card_cons]

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