edgeSet_map — Mathlib

English

edge set of a mapped subgraph equals the image of the original edge set under the Sym2 map.

Русский

Множество рёбер отображённого подграфа равно образу исходного множества рёбер подстановкой Sym2.map.

LaTeX

$$$ (H.map f).edgeSet = \text{Sym2.map } f '' H.edgeSet $$$

Lean4

@[simp]
theorem edgeSet_map (f : G →g G') (H : G.Subgraph) : (H.map f).edgeSet = Sym2.map f '' H.edgeSet :=
  Sym2.fromRel_relationMap ..

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