Theorems · Theorem · functional analysis

norm_inner_eq_norm_tfae

∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E),
  [‖inner 𝕜 x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner 𝕜 x y / inner 𝕜 x x) • x, x = 0 ∨ ∃ r, y = r • x,
      x = 0 ∨ y ∈ 𝕜 ∙ x].TFAE

Defined in

Mathlib.Analysis.InnerProductSpace.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

RCLikeNormedAddCommGroupInnerProductSpace