Theorems · Definition · order theory

AddQuantale.noConfusion

{P : Sort u} →
  {α : Type u_1} →
    {inst : AddSemigroup α} →
      {inst_1 : CompleteLattice α} →
        {inst_2 : IsAddQuantale α} →
          {t : AddQuantale α} →
            {α' : Type u_1} →
              {inst' : AddSemigroup α'} →
                {inst'_1 : CompleteLattice α'} →
                  {inst'_2 : IsAddQuantale α'} →
                    {t' : AddQuantale α'} →
                      α = α' →
                        inst ≍ inst' → inst_1 ≍ inst'_1 → inst_2 ≍ inst'_2 → t ≍ t' → AddQuantale.noConfusionType P t t'

Defined in

Mathlib.Algebra.Order.Quantale

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms