English
There is an embedding between a graph G on V and the mapped graph G.map f along an injective f : V ≃ W, realized as a graph isomorphism G ≃g G.map f.toEmbedding.
Русский
Существует вложение графа G на V в граф, полученный из G.mapping через отображение f : V ≃ W, реализующее изоморфизм графов между G и G.map f.toEmbedding.
LaTeX
$$$$G \\;\\cong_g\\; G.map\\; f^{\\mathrm{toEmbedding}}$$$$
Lean4
/-- Given an injective function, there is an embedding from a graph into the mapped graph. -/
-- Porting note: `@[simps]` does not work here anymore since `f` is not a constructor application.
-- `@[simps toEmbedding]` could work, but Floris suggested writing `map_apply` for now.
protected def map (f : V ≃ W) (G : SimpleGraph V) : G ≃g G.map f.toEmbedding :=
{ f with map_rel_iff' := by simp }
