edgeSet_map — Mathlib

English

The edge set of a mapped walk equals the image of the original edge set under the induced map on Sym2-edges.

Русский

Множество ребер образованного обхода равно образу исходного множества ребер под соответствующим отображением на Sym2-ребра.

LaTeX

$$(p.map f).edgeSet = Set.image (Sym2.map (RelHom.instFunLike.coe f)) p.edgeSet$$

Lean4

@[simp]
theorem edgeSet_map : (p.map f).edgeSet = Sym2.map f '' p.edgeSet := by ext; simp

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