edgeFinset_map — Mathlib

English

Mapping a graph along an embedding f preserves the edgeFinset after applying the corresponding sym2Map. That is, (G.map f).edgeFinset = G.edgeFinset.map f.sym2Map.

Русский

Отображение графа по отображению f сохраняет множество рёбер после применения соответствующего отображения Sym2.

LaTeX

$$(G.map f).edgeFinset = G.edgeFinset.map f.sym2Map$$

Lean4

@[simp]
theorem edgeFinset_map (f : V ↪ W) (G : SimpleGraph V) [DecidableRel G.Adj] :
    (G.map f).edgeFinset = G.edgeFinset.map f.sym2Map :=
  by
  rw [Finset.map_eq_image, ← Set.toFinset_image, Set.toFinset_inj]
  exact G.edgeSet_map f

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