Theorems · Definition · functional analysis

PositiveLinearMap.PreGNS

{A : Type u_1} → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (A →ₚ[ℂ] ℂ) → Type u_1

The Gelfand─Naimark─Segal (GNS) space constructed from a positive linear functional on a non-unital C⋆-algebra. This is a type synonym of A. This space is only a pre-inner product space. Its Hilbert space completion is PositiveLinearMap.GNS.

Defined in

Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal

Cited by

10 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrder