map_append — Mathlib

English

Mapping distributes over concatenation of walks: f(p ∔ q) = f(p) ∔ f(q).

Русский

Отображение распределяется по конкатенации обходов: f(p ∔ q) = f(p) ∔ f(q).

LaTeX

$$$\\text{map}\, f\\,(p\\;\\append\\; q) = (\\text{map}\\, f\\, p)\\;\\append\\; (\\text{map}\\, f\\, q)$$$

Lean4

theorem map_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).map f = (p.map f).append (q.map f) := by
  induction p <;> simp [*]

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