linearProjOfIsCompl_apply_eq_zero_iff

Mathlib.LinearAlgebra.Projection

URI: https://scilib.ai/kg/mathlib#Submodule.linearProjOfIsCompl_apply_eq_zero_iff

← MathLib Explorer

English

For any x ∈ E, linearProjOfIsCompl p q h x = 0 if and only if x ∈ q.

Русский

Для любого x ∈ E линейная проекция равна нулю тогда и только тогда, когда x ∈ q.

LaTeX

$$$linearProjOfIsCompl\; p\; q\; h\; x = 0 \iff x \in q$$$

Lean4

@[simp]
theorem linearProjOfIsCompl_apply_eq_zero_iff (h : IsCompl p q) {x : E} : linearProjOfIsCompl p q h x = 0 ↔ x ∈ q := by
  simp [linearProjOfIsCompl]

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

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

Разделы

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

Аффилиация

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