linearProjOfIsCompl_isCompl_projection

English

For all x ∈ E, linearProjOfIsCompl p q h (h.projection x) = linearProjOfIsCompl p q h x.

Русский

Для всех x ∈ E линейная проекция при применении к h.projection(x) равна самой линейной проекции на x.

LaTeX

$$$\forall x\in E:\; linearProjOfIsCompl p q h (h.projection x) = linearProjOfIsCompl p q h x$$$

Lean4

theorem linearProjOfIsCompl_isCompl_projection (h : IsCompl p q) (x : E) :
    linearProjOfIsCompl p q h (h.projection x) = linearProjOfIsCompl p q h x :=
  linearProjOfIsCompl_apply_left h _

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