English
Let f be a copy of A into B and let A' be a subgraph of A. Then A' is isomorphic to its image under the copy map, i.e. there exists a graph isomorphism between A' and its image (A'.map f.toHom).coe.
Русский
Пусть f есть копия графа A в B, и пусть A' — подграф A. Тогда A' изоморфен своему образу под копированием, т.е. существует графовая изоморфия между A' и изображением A' под отображением f.toHom.
LaTeX
$$$A' \cong_g (A'.map\; f.toHom).coe$$$
Lean4
/-- The isomorphism from a subgraph of `A` to its map under a copy `f : Copy A B`. -/
noncomputable def isoSubgraphMap (f : Copy A B) (A' : A.Subgraph) : A'.coe ≃g (A'.map f.toHom).coe :=
by
use Equiv.Set.image f.toHom _ f.injective
simp_rw [Subgraph.map_verts, Equiv.Set.image_apply, Subgraph.coe_adj, Subgraph.map_adj, Relation.map_apply,
f.injective.eq_iff, exists_eq_right_right, exists_eq_right, forall_true_iff]
