Theorems · Theorem · functional analysis

orthogonalFamily_iff_pairwise

∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) ↔ Pairwise (Function.onFun (fun x1 x2 => x1 ⟂ x2) V)

Defined in

Mathlib.Analysis.InnerProductSpace.Orthogonal

Cited by

2 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpace