Theorems · Theorem · functional analysis

CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto

∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {l : Filter A},
  (∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Filter.Tendsto (fun x => x * m) l (nhds m)) →
    ∀ (m : A), Filter.Tendsto (fun x => x * m) l (nhds m)

To show that l is a one-sided approximate unit for A, it suffices to verify it only for m : A with 0 ≤ m and ‖m‖ < 1.

Defined in

Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrderStarOrderedRing