pi_proj

Mathlib.LinearAlgebra.Pi

URI: https://scilib.ai/kg/mathlib#LinearMap.pi_proj

English

The projection operator on i yields the i-th coordinate function.

Русский

Проекция на i даёт i-ю координатную функцию.

LaTeX

$$proj_apply$$

Lean4

@[simp]
theorem pi_proj : pi proj = LinearMap.id (R := R) (M := ∀ i, φ i) :=
  rfl

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

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

Разделы

Аффилиация

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