mapLe_isTrail — Mathlib

English

If h is an inclusion of graphs, then p.mapLe h preserves the IsTrail property, i.e., (p.mapLe h).IsTrail iff p.IsTrail.

Русский

Если h — вложение графов, отображение p.mapLe h сохраняет свойство IsTrail, то есть (p.mapLe h).IsTrail эквивалентно p.IsTrail.

LaTeX

$$$ \forall {G G' : SimpleGraph V} (h : G \le G') {u v : V} {p : G.Walk u v}, \n \text{mapLe isTrail equivalence}\n \Rightarrow (p.mapLe h).IsTrail \iff p.IsTrail$$$

Lean4

@[simp]
theorem mapLe_isTrail {G G' : SimpleGraph V} (h : G ≤ G') {u v : V} {p : G.Walk u v} :
    (p.mapLe h).IsTrail ↔ p.IsTrail :=
  map_isTrail_iff_of_injective Function.injective_id

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