card_edgeFinset_replaceVertex_of_not_adj

English

The cardinality satisfies #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + deg(s) − deg(t).

Русский

Число элементов edgeFinset после замены при отсутствии смежности равно #G.edgeFinset + deg(s) − deg(t).

LaTeX

$$$ \#(G.replaceVertex s t).edgeFinset = \#G.edgeFinset + \deg(s) - \deg(t) $$$

Lean4

theorem card_edgeFinset_replaceVertex_of_not_adj (hn : ¬G.Adj s t) :
    #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t :=
  by
  have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
  rw [G.edgeFinset_replaceVertex_of_not_adj hn, card_union_of_disjoint G.disjoint_sdiff_neighborFinset_image,
    card_sdiff_of_subset inc, ← Nat.sub_add_comm <| card_le_card inc, card_incidenceFinset_eq_degree]
  congr 2
  rw [card_image_of_injective, card_neighborFinset_eq_degree]
  unfold Function.Injective
  aesop

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