Theorems · Definition · functional analysis

CStarAlgebra.approximateUnit

(A : Type u_1) → [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → [StarOrderedRing A] → Filter A

The canonical approximate unit in a C⋆-algebra generated by the basis of sets {x | a ≤ x} ∩ closedBall 0 1 for 0 ≤ a. See also CStarAlgebra.hasBasis_approximateUnit.

Defined in

Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Cited by

2 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderStarOrderedRing