projection_apply — Mathlib

English

The projection hpq equals the canonical projection p.linearProjOfIsCompl q hpq when viewed as functions E → p.

Русский

Проекция hpq равна канонической линейной проекции p.linearProjOfIsCompl q hpq, когда рассматривается как отображение E → p.

LaTeX

$$$hpq.\text{projection}(x) = p.\text{linearProjOfIsCompl } q\ hpq\; x$$$

Lean4

theorem projection_apply (hpq : IsCompl p q) (x : E) : hpq.projection x = p.linearProjOfIsCompl q hpq x :=
  rfl

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