Theorems · Theorem · functional analysis

OrthogonalFamily.sum_projection_of_mem_iSup

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : Fintype ι] {V : ι → Submodule 𝕜 E} [inst_4 : ∀ (i : ι), CompleteSpace ↥(V i)],
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) → ∀ x ∈ iSup V, ∑ i, (V i).starProjection x = x

If x lies within an orthogonal family v, it can be expressed as a sum of projections.

Defined in

Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional

Cited by

0 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceFintypeCompleteSpace