map_isPath_of_injective — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem map_isPath_of_injective (hinj : Function.Injective f) (hp : p.IsPath) : (p.map f).IsPath := by
  induction p with
  | nil => simp
  | cons _ _ ih =>
    rw [Walk.cons_isPath_iff] at hp
    simp only [map_cons, cons_isPath_iff, ih hp.1, support_map, List.mem_map, not_exists, not_and, true_and]
    intro x hx hf
    cases hinj hf
    exact hp.2 hx

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