id_eq_sum_starProjection_self_orthogonalComplement

English

For a complete space E and subspace K with an orthogonal projection, the identity equals the sum of the two star projections onto K and K⊥.

Русский

В полном пространстве E с ортогональной проекцией, тождество равно сумме звездочных проекций на K и на K⊥.

LaTeX

$$$ \mathrm{id}_E = K.starProjection + K^{\perp}.starProjection. $$$

Lean4

/-- In a complete space `E`, the projection maps onto a complete subspace `K` and its orthogonal
complement sum to the identity. -/
theorem id_eq_sum_starProjection_self_orthogonalComplement [K.HasOrthogonalProjection] :
    ContinuousLinearMap.id 𝕜 E = K.starProjection + Kᗮ.starProjection :=
  by
  ext w
  exact (K.starProjection_add_starProjection_orthogonal w).symm

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