linearProjOfIsCompl_apply_right'

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#Submodule.linearProjOfIsCompl_apply_right'

← MathLib Explorer

English

If x ∈ q, then linearProjOfIsCompl p q h x = 0.

Русский

Если x ∈ q, то линейная проекция на p вдоль q отправляет x в 0.

LaTeX

$$$x\in q \Rightarrow linearProjOfIsCompl p q h x = 0$$$

Lean4

theorem linearProjOfIsCompl_apply_right' (h : IsCompl p q) (x : E) (hx : x ∈ q) : linearProjOfIsCompl p q h x = 0 :=
  (linearProjOfIsCompl_apply_eq_zero_iff h).2 hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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