Theorems · Definition · functional analysis

CompletelyPositiveMap.mk.noConfusion

{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₂} →
                {P : Sort u} →
                  {toLinearMap : A₁ →ₗ[ℂ] A₂} →
                    {map_cstarMatrix_nonneg' :
                        ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap} →
                      {toLinearMap' : A₁ →ₗ[ℂ] A₂} →
                        {map_cstarMatrix_nonneg'' :
                            ∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap'} →
                          { toLinearMap := toLinearMap, map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg' } =
                              { toLinearMap := toLinearMap', map_cstarMatrix_nonneg' := map_cstarMatrix_nonneg'' } →
                            (toLinearMap ≍ toLinearMap' → P) → P

Defined in

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Cited by

1 results in Mathlib

Foundations

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