map_injective_of_injective — Mathlib

English

If the edge-map is injective on the underlying graph, then the walk-map is injective.

Русский

Если отображение рёбер на графе инъективно, то отображение обхода инъективно.

LaTeX

$$Injectivity of Walk.map f follows from Injective f on vertices: (Walk.map f) is injectable.$$

Lean4

theorem map_injective_of_injective {f : G →g G'} (hinj : Function.Injective f) (u v : V) :
    Function.Injective (Walk.map f : G.Walk u v → G'.Walk (f u) (f v)) :=
  by
  intro p p' h
  induction p with
  | nil =>
    cases p'
    · rfl
    · simp at h
  | cons _ _ ih =>
    cases p' with
    | nil => simp at h
    | cons _ _ =>
      simp only [map_cons, cons.injEq] at h
      cases hinj h.1
      simp only [cons.injEq, heq_iff_eq, true_and]
      apply ih
      simpa using h.2

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