Theorems · Inductive type · functional analysis

InnerProductSpace

(𝕜 : Type u_4) → (E : Type u_5) → [RCLike 𝕜] → [SeminormedAddCommGroup E] → Type (max u_4 u_5)

A (pre) inner product space is a vector space with an additional operation called inner product. The (semi)norm could be derived from the inner product, instead we require the existence of a seminorm and the fact that ‖x‖^2 = re ⟪x, x⟫ to be able to put instances on 𝕂 or product spaces. Note that NormedSpace does not assume that ‖x‖=0 implies x=0 (it is rather a seminorm). To construct a seminorm from an inner product, see PreInnerProductSpace.ofCore.

Defined in

Mathlib.Analysis.InnerProductSpace.Defs

Cited by

3,523 results in Mathlib

Foundations

Depth 2 from the axioms, rests on 4 definitions · uses no axioms

Assumes

RCLikeSeminormedAddCommGroup