mapLe_isCycle — Mathlib

English

Let G ≤ G' and p be a walk in G starting and ending at the same vertex. Then (p.mapLe h) is a cycle in G' if and only if p is a cycle in G.

Русский

Пусть G ≤ G' и p — цикл-путь в G (начальная и конечная вершины совпадают). Тогда p.mapLe h является циклом в G' тогда и только тогда, когда p является циклом в G.

LaTeX

$$$\\\\forall {V} {G G' : SimpleGraph\,V} (h : G \\\\le G') {u : V} {p : G.Walk u u}, \\\\ (p.mapLe h).IsCycle \\\\leftrightarrow p.IsCycle$$

Lean4

@[simp]
theorem mapLe_isCycle {G G' : SimpleGraph V} (h : G ≤ G') {u : V} {p : G.Walk u u} : (p.mapLe h).IsCycle ↔ p.IsCycle :=
  map_isCycle_iff_of_injective Function.injective_id

Похожие утверждения