projection_range

Mathlib.LinearAlgebra.Projection

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

English

The range of the projection associated to IsCompl hpq equals p.

Русский

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

LaTeX

$$$\operatorname{range}(Submodule.IsCompl.projection\; hpq) = p$$$

Lean4

@[simp]
theorem projection_range (hpq : IsCompl p q) : range hpq.projection = p := by simp [projection, range_comp]

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

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

Разделы

Аффилиация

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