projection_apply_left

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#Submodule.IsCompl.projection_apply_left

English

The range of linearProjOfIsCompl is all of p.

Русский

Область значений линейной проекции на p равна всей p.

LaTeX

$$$\operatorname{range}(linearProjOfIsCompl p q h) = \top$ (in p)$$

Lean4

@[simp]
theorem projection_apply_left (hpq : IsCompl p q) (x : p) : hpq.projection x = x := by simp [projection]

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

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

Разделы

Аффилиация

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