nodup_support — Mathlib

English

If f is injective, then mapping a path preserves the IsPath property, i.e., p.IsPath implies (p.map f).IsPath.

Русский

Если отображение f инъективно, то отображение пути сохраняет свойство IsPath, то есть если p является путём, то p.map f также является путём.

LaTeX

$$$ \forall {V} {V'} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G \rightarrow_g G'} {u v : V} {p : G.Walk u v}, \text{Function.Injective } f \to p.IsPath \to (p.map f).IsPath$$$

Lean4

@[simp]
theorem nodup_support {u v : V} (p : G.Path u v) : (p : G.Walk u v).support.Nodup :=
  (Walk.isPath_def _).mp p.property

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