coe_proj

Mathlib.Topology.Algebra.Module.LinearMapPiProd

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

English

The product map f1.prodMap f2 is the continuous linear map sending (x,y) ↦ (f1 x, f2 y).

Русский

Произведение отображения создает отображение (x,y) ↦ (f1 x, f2 y).

LaTeX

$$$(f_1 \\prodMap f_2)(x,y) = (f_1 x, f_2 y)$$$

Lean4

@[simp]
theorem coe_proj (i : ι) : (proj i).toLinearMap = (LinearMap.proj i : ((i : ι) → φ i) →ₗ[R] _) :=
  rfl

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

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

Разделы

Аффилиация

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