Theorems · Definition · functional analysis

CompletelyPositiveMap.noConfusion

{P : Sort u} →
  {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₂} →
                  {t : CompletelyPositiveMap A₁ A₂} →
                    {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₂'} →
                                    {t' : CompletelyPositiveMap A₁' A₂'} →
                                      A₁ = A₁' →
                                        A₂ = A₂' →
                                          inst ≍ inst' →
                                            inst_1 ≍ inst'_1 →
                                              inst_2 ≍ inst'_2 →
                                                inst_3 ≍ inst'_3 →
                                                  inst_4 ≍ inst'_4 →
                                                    inst_5 ≍ inst'_5 →
                                                      t ≍ t' → CompletelyPositiveMap.noConfusionType P t t'

Defined in

Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap

Cited by

0 results in Mathlib

Foundations

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