lmap_lof

Mathlib.Algebra.DirectSum.Module

URI: https://scilib.ai/kg/mathlib#DirectSum.lmap_lof

← MathLib Explorer

English

The map lmap applied to lof_i(b) equals lof_i(f_i(b)).

Русский

Применение lmap к lof_i(b) даёт lof_i(f_i(b)).

LaTeX

$$$\\mathrm{lmap}\\ f\\ (\\mathrm{lof}\\,i\\ (b)) = \\mathrm{lof}\\,i\\ (f_i(b)).$$$

Lean4

@[simp]
theorem lmap_lof [DecidableEq ι] (i) (x : M i) : lmap f (lof R _ _ _ x) = lof R _ _ _ (f i x) :=
  DFinsupp.mapRange_single (hf := fun _ ↦ map_zero _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru