coe_continuous_linearProjOfClosedCompl

English

If p and q are complementary closed subspaces of E, then the linear projection onto p along q from the closed-complement construction equals the projection from the IsCompl construction.

Русский

Пусть p и q — замкнутые комплементные подпсрстранства пространства E. Тогда линейная проекция на p вдоль q, полученная через замкнутое дополнение, совпадает с проекцией через IsCompl.

LaTeX

$$$p\text{.linearProjOfClosedCompl } q h hp hq = p\text{.linearProjOfIsCompl } q h$$$

Lean4

@[simp]
theorem coe_continuous_linearProjOfClosedCompl (h : IsCompl p q) (hp : IsClosed (p : Set E))
    (hq : IsClosed (q : Set E)) : (p.linearProjOfClosedCompl q h hp hq : E →ₗ[𝕜] p) = p.linearProjOfIsCompl q h :=
  rfl

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