edgeFinset_replaceVertex_of_adj — Mathlib

English

Auxiliary lemmas about Finset conversions for the not-adjacent replacement case.

Русский

Дополнительные леммы о конверсиях Finset для случая замены при отсутствии смежности.

LaTeX

$$$ \text{Auxiliary finset identities for not-adjacent replacement}$$$

Lean4

theorem edgeFinset_replaceVertex_of_adj (ha : G.Adj s t) :
    (G.replaceVertex s t).edgeFinset =
      (G.edgeFinset \ G.incidenceFinset t ∪ (G.neighborFinset s).image (s(·, t))) \ {s(t, t)} :=
  by
  simp only [incidenceFinset, neighborFinset, ← Set.toFinset_diff, ← Set.toFinset_image, ← Set.toFinset_union,
    ← Set.toFinset_singleton]
  exact Set.toFinset_congr (G.edgeSet_replaceVertex_of_adj ha)

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