map_of — Mathlib

English

The map on a direct sum sends the embedded element in the i-th summand to the corresponding embedded image in the target summand.

Русский

Гомоморфизм DirectSum переводит вложенную в i-ю компонента элемент в соответствующее изображение в целевой компоненте.

LaTeX

$$$$\\mathrm{map}\, f\\big(\\mathrm{DirectSum.of}\\; \\alpha\\; i\\; x\\right) = \\mathrm{DirectSum.of}\\; \\beta\\; i\\; (f_i(x)).$$$$

Lean4

@[simp]
theorem map_of [DecidableEq ι] (i : ι) (x : α i) : map f (of α i x) = of β i (f i x) :=
  DFinsupp.mapRange_single (hf := fun _ => map_zero _)

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