Theorems · Inductive type · functional analysis

Filter.IsIncreasingApproximateUnit

{A : Type u_1} → [NonUnitalCStarAlgebra A] → [PartialOrder A] → Filter A → Prop

An increasing approximate unit in a C⋆-algebra is an approximate unit contained in the closed unit ball of nonnegative elements.

Defined in

Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Cited by

9 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

NonUnitalCStarAlgebraPartialOrder