Theorems · Definition · functional analysis

NonUnitalCommCStarAlgebra.noConfusion

{P : Sort u} →
  {A : Type u_1} →
    {t : NonUnitalCommCStarAlgebra A} →
      {A' : Type u_1} →
        {t' : NonUnitalCommCStarAlgebra A'} → A = A' → t ≍ t' → NonUnitalCommCStarAlgebra.noConfusionType P t t'

Defined in

Mathlib.Analysis.CStarAlgebra.Classes

Cited by

0 results in Mathlib

Foundations

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