Theorems · Theorem · functional analysis

CStarAlgebra.hasBasis_approximateUnit

∀ (A : Type u_1) [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [inst_2 : StarOrderedRing A],
  (CStarAlgebra.approximateUnit A).HasBasis (fun x => 0 ≤ x ∧ ‖x‖ < 1) fun x => {x_1 | x ≤ x_1} ∩ Metric.closedBall 0 1

The canonical approximate unit in a C⋆-algebra has a basis of sets {x | a ≤ x} ∩ closedBall 0 1 for 0 ≤ a.

Defined in

Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Cited by

1 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderStarOrderedRing