English
For any f: V ↪ W and G: SimpleGraph V, the edge set of the mapped graph equals the image of the original edge set under the induced sym2Map: (G.map f).edgeSet = f.sym2Map '' G.edgeSet.
Русский
Для вложения f: V ↪ W и графа G: SimpleGraph V множество рёбер отображенного графа равно образу множества рёбер исходного графа под симметрическим отображением f.sym2Map: (G.map f).edgeSet = f.sym2Map '' G.edgeSet.
LaTeX
$$$$ (G.map f).edgeSet = f.sym2Map '' G.edgeSet. $$$$
Lean4
theorem comap_symm (G : SimpleGraph V) (e : V ≃ W) : G.comap e.symm.toEmbedding = G.map e.toEmbedding := by ext;
simp only [Equiv.apply_eq_iff_eq_symm_apply, comap_adj, map_adj, Equiv.toEmbedding_apply, exists_eq_right_right,
exists_eq_right]
