English
If f is an injective graph homomorphism from G to G', then the induced map on G-paths, Path.map f hinj, is injective from G.Path u v to G'.Path (f u) (f v).
Русский
Если g является инъективным отображением графов G в G', то индуцированное отображение на пути Path.map f hinj является инъекцией от путей G.Path u v в G'.Path (f u) (f v).
LaTeX
$$$\\\\forall {V} {G G' : SimpleGraph\,V} {f : G \\to G'} (hinj : Function.Injective f) {u v : V}, \\\\ Injective (Path.map f hinj)$$
Lean4
theorem map_injective {f : G →g G'} (hinj : Function.Injective f) (u v : V) :
Function.Injective (Path.map f hinj : G.Path u v → G'.Path (f u) (f v)) :=
by
rintro ⟨p, hp⟩ ⟨p', hp'⟩ h
simp only [Path.map, Subtype.mk.injEq] at h
simp [Walk.map_injective_of_injective hinj u v h]
