English
An isomorphism f : G ≃g G' induces an equivalence between their edge sets: mapEdgeSet f : G.edgeSet ≃ G'.edgeSet.
Русский
Изоморфизм f : G ≃g G' порождает эквивалентность множеств ребер: mapEdgeSet f : G.edgeSet ≃ G'.edgeSet.
LaTeX
$$$ G.edgeSet \cong G'.edgeSet $$$
Lean4
/-- An isomorphism of graphs induces an equivalence of edge sets. -/
@[simps]
def mapEdgeSet : G.edgeSet ≃ G'.edgeSet where
toFun := Hom.mapEdgeSet f
invFun := Hom.mapEdgeSet f.symm
left_inv := by
rintro ⟨e, h⟩
simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Embedding.toFun_eq_coe, RelEmbedding.coe_toEmbedding,
RelIso.coe_toRelEmbedding, Sym2.map_map, comp_apply, Subtype.mk.injEq]
convert congr_fun Sym2.map_id e
exact RelIso.symm_apply_apply _ _
right_inv := by
rintro ⟨e, h⟩
simp only [Hom.mapEdgeSet, RelEmbedding.toRelHom, Embedding.toFun_eq_coe, RelEmbedding.coe_toEmbedding,
RelIso.coe_toRelEmbedding, Sym2.map_map, comp_apply, Subtype.mk.injEq]
convert congr_fun Sym2.map_id e
exact RelIso.apply_symm_apply _ _
