English
Let G be a subgraph of G' (G ≤ G') and p a walk from u to v in G. Then the image of p under the inclusion map, denoted p.mapLe h, is a walk from u to v in G'. Moreover, p.mapLe h is a path if and only if p is a path.
Русский
Пусть G является подграфом G' (G ≤ G') и p —Walk от u до v в G. Тогда образ p под включениям отображается как p.mapLe h и является путём от u к v в G'. При этом p.mapLe h является путём тогда и только тогда, когда p является путём.
LaTeX
$$$\\\\forall {V} {G G' : SimpleGraph\,V} (h : G \\\\le G') {u v : V} {p : G.Walk u v}, \\\\ (p.mapLe h).IsPath \\\\leftrightarrow p.IsPath$$
Lean4
@[simp]
theorem mapLe_isPath {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} : (p.mapLe h).IsPath ↔ p.IsPath :=
map_isPath_iff_of_injective Function.injective_id
