Theorems · Definition · functional analysis

Filter.IsIncreasingApproximateUnit.casesOn

{A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      {l : Filter A} →
        {motive : l.IsIncreasingApproximateUnit → Sort u} →
          (t : l.IsIncreasingApproximateUnit) →
            ((toIsApproximateUnit : l.IsApproximateUnit) →
                (eventually_nonneg : ∀ᶠ (x : A) in l, 0 ≤ x) →
                  (eventually_norm : ∀ᶠ (x : A) in l, ‖x‖ ≤ 1) → motive ⋯) →
              motive t

Defined in

Mathlib.Analysis.CStarAlgebra.ApproximateUnit

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraPartialOrder