map_updateCol — Mathlib

English

For DecidableEq n, (f : α → β) satisfies map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c).

Русский

Для DecidableEq n: map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c).

LaTeX

$$$ \mathrm{map}\ (\mathrm{updateCol}\ M\ j\ c)\ f = \mathrm{updateCol}\ (M.map f)\ j (f \circ c) $$$

Lean4

theorem map_updateCol [DecidableEq n] (f : α → β) : map (updateCol M j c) f = updateCol (M.map f) j (f ∘ c) :=
  by
  ext
  rw [updateCol_apply, map_apply, map_apply, updateCol_apply]
  exact apply_ite f _ _ _

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