Theorems · Theorem · functional analysis

Submodule.norm_eq_iInf_iff_inner_eq_zero

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) {u v : E}, v ∈ K → (‖u - v‖ = ⨅ w, ‖u - ↑w‖ ↔ ∀ w ∈ K, inner 𝕜 (u - v) w = 0)

Characterization of minimizers in the projection on a subspace. Let u be a point in an inner product space, and let K be a nonempty subspace. Then point v minimizes the distance ‖u - v‖ over points in K if and only if for all w ∈ K, ⟪u - v, w⟫ = 0 (i.e., u - v is orthogonal to the subspace K)

Defined in

Mathlib.Analysis.InnerProductSpace.Projection.Minimal

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpace