map_updateRow — Mathlib

English

For DecidableEq m, (f : α → β) satisfies map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b).

Русский

Для DecidableEq m: map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b).

LaTeX

$$$ \mathrm{map}\ (\mathrm{updateRow}\ M\ i\ b)\ f = \mathrm{updateRow}\ (M.map f)\ i\ (f \circ b) $$$

Lean4

theorem map_updateRow [DecidableEq m] (f : α → β) : map (updateRow M i b) f = updateRow (M.map f) i (f ∘ b) :=
  by
  ext
  rw [updateRow_apply, map_apply, map_apply, updateRow_apply]
  exact apply_ite f _ _ _

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