proj_pi

Mathlib.Topology.Algebra.Module.LinearMapPiProd

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.proj_pi

English

The i-th projection composed with the pi construction returns the i-th map f_i: (proj i) ∘ (pi f) = f_i.

Русский

i-я проекция после pi-конструкции возвращает i-ю отображение f_i: (proj i) ∘ (pi f) = f_i.

LaTeX

$$$(proj i) \\circ (\\pi f) = f_i$$$

Lean4

@[simp]
theorem proj_pi (f : ∀ i, M₂ →L[R] φ i) (i : ι) : (proj i).comp (pi f) = f i :=
  rfl

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

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

Разделы

Аффилиация

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