orthogonalProjection_comp_subtypeL

English

If K is complete, every v ∈ E can be written as y + z with y ∈ K and z ∈ Kᗮ.

Русский

Если K полно, то любой вектор v в E разлагается на v = y + z с y ∈ K и z ∈ Kᗮ.

LaTeX

$$$ \exists y \in K, \ exists z \in K^{\perp}, \ v = y + z $$$

Lean4

/-- The projection into `U` from an orthogonal submodule `V` is the zero map. -/
theorem orthogonalProjection_comp_subtypeL {U V : Submodule 𝕜 E} [U.HasOrthogonalProjection] (h : U ⟂ V) :
    U.orthogonalProjection ∘L V.subtypeL = 0 :=
  ContinuousLinearMap.ext fun v => orthogonalProjection_mem_subspace_orthogonalComplement_eq_zero <| h.symm v.prop

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