Theorems · Definition · functional analysis

Submodule.orthogonalProjectionFn

Deprecated since 2026-06-10Mathlib marks this declaration as deprecated.

{𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] → {K : Submodule 𝕜 E} → [K.HasOrthogonalProjection] → E → E

The orthogonal projection onto a complete subspace, as an unbundled function. This definition is only intended for use in setting up the bundled version orthogonalProjection and should not be used once that is defined.

Defined in

Mathlib.Analysis.InnerProductSpace.Projection.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpaceSubmodule.HasOrthogonalProjection