projection_apply_eq_zero_iff

Mathlib.LinearAlgebra.Projection

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

← MathLib Explorer

English

The IsCompl projection hpq satisfies hpq.projection x = 0 iff x ∈ q.

Русский

Проекция IsCompl hpq удовлетворяет hpq.projection x = 0 тогда и только тогда, когда x ∈ q.

LaTeX

$$$hpq.projection(x)=0 \iff x\in q$$$

Lean4

@[simp]
theorem projection_apply_eq_zero_iff (hpq : IsCompl p q) {x : E} : hpq.projection x = 0 ↔ x ∈ q := by
  simp [projection, -coe_linearProjOfIsCompl_apply]

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

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

Разделы

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

Аффилиация

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