apply_eq_component

Mathlib.Algebra.DirectSum.Module

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

English

For any f in the direct sum, its i-th coordinate equals the i-th projection applied to f; i.e. f_i = π_i(f).

Русский

Для любого элемента f прямой суммы его i-я координата равна применению к нему i-й проекции: f_i = π_i(f).

LaTeX

$$$f_i = \\mathrm{component}_i(f).$$$

Lean4

theorem apply_eq_component (f : ⨁ i, M i) (i : ι) : f i = component R ι M i f :=
  rfl

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

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

Разделы

Аффилиация

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