card_edgeFinset_replaceVertex_of_adj

English

If G.Adj s t, then #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + deg(s) − deg(t) − 1.

Русский

Если G.Adj s t, тогда #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + deg(s) − deg(t) − 1.

LaTeX

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

Lean4

theorem card_edgeFinset_replaceVertex_of_adj (ha : G.Adj s t) :
    #(G.replaceVertex s t).edgeFinset = #G.edgeFinset + G.degree s - G.degree t - 1 :=
  by
  have inc : G.incidenceFinset t ⊆ G.edgeFinset := by simp [incidenceFinset, incidenceSet_subset]
  rw [G.edgeFinset_replaceVertex_of_adj ha, card_sdiff_of_subset (by simp [ha]),
    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

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