A subspace and its orthogonal complement split the space (Three.VI.3)

Open

hefferon_orthogonal_projection_decomposition

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

gram-schmidtinner-productlinear-algebraorthogonal-projection

Let $S$ be a subspace of a finite-dimensional real inner product space. Then $S$ and its orthogonal complement $S^{\perp}$ are complementary: they intersect trivially and together span the whole space, so every vector decomposes uniquely as its orthogonal projection into $S$ plus a vector orthogonal to $S$ .

Preamble

import Definitions.Def_hefferon_prelude

open Matrix
open HefferonLinAlg

Formal statement

theorem hefferon_orthogonal_projection_decomposition
    {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V]
    (S : Submodule ℝ V) :
    IsCompl S Sᗮ := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Three, Section VI.3, Theorem 3.4, p. 298

View graph