Theorems · Definition · functional analysis

CompletelyPositiveMap.casesOn

{A₁ : Type u_1} →
  {A₂ : Type u_2} →
    [inst : NonUnitalCStarAlgebra A₁] →
      [inst_1 : NonUnitalCStarAlgebra A₂] →
        [inst_2 : PartialOrder A₁] →
          [inst_3 : PartialOrder A₂] →
            [inst_4 : StarOrderedRing A₁] →
              [inst_5 : StarOrderedRing A₂] →
                {motive : CompletelyPositiveMap A₁ A₂ → Sort u} →
                  (t : CompletelyPositiveMap A₁ A₂) →
                    ((toLinearMap : A₁ →ₗ[ℂ] A₂) →
                        (map_cstarMatrix_nonneg' :
                            ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap) →
                          motive { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' }) →
                      motive t

Defined in

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Cited by

0 results in Mathlib

Foundations

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

Assumes

NonUnitalCStarAlgebraNonUnitalCStarAlgebraPartialOrderPartialOrderStarOrderedRingStarOrderedRing