coe_pi'

Mathlib.Topology.Algebra.Module.LinearMapPiProd

URI: https://scilib.ai/kg/mathlib#ContinuousLinearMap.coe_pi'

English

The function underlying pi f equals the coordinate-wise evaluation: its i-th coordinate is f_i applied to the input.

Русский

Приведение к функции pi f равно координатной оценке: i-я координата равна f_i(ввод).

LaTeX

$$$\\bigl(\\pi f\\bigr)(x)_i = f_i(x)$$$

Lean4

@[simp]
theorem coe_pi' (f : ∀ i, M →L[R] φ i) : ⇑(pi f) = fun c i => f i c :=
  rfl

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

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

Разделы

Аффилиация

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