map_mem_edgeSet — Mathlib

English

If an edge e lies in the edge set of G, its image under f lies in the edge set of G'.

Русский

Если ребро e принадлежит множеству ребер G, то его образ под действием f принадлежит множеству ребер G'.

LaTeX

$$$ {e \\in G.edgeSet} \\Rightarrow {e.map\\ f \\in G'.edgeSet} $$$

Lean4

theorem map_mem_edgeSet {e : Sym2 V} (h : e ∈ G.edgeSet) : e.map f ∈ G'.edgeSet :=
  Sym2.ind (fun _ _ => f.map_rel') e h

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