Theorems · Definition · order theory

OrderMonoidWithZeroHom.mk.noConfusion

{α : Type u_6} →
  {β : Type u_7} →
    {inst : Preorder α} →
      {inst_1 : Preorder β} →
        {inst_2 : MulZeroOneClass α} →
          {inst_3 : MulZeroOneClass β} →
            {P : Sort u} →
              {toMonoidWithZeroHom : α →*₀ β} →
                {monotone' : Monotone (↑toMonoidWithZeroHom).toFun} →
                  {toMonoidWithZeroHom' : α →*₀ β} →
                    {monotone'' : Monotone (↑toMonoidWithZeroHom').toFun} →
                      { toMonoidWithZeroHom := toMonoidWithZeroHom, monotone' := monotone' } =
                          { toMonoidWithZeroHom := toMonoidWithZeroHom', monotone' := monotone'' } →
                        (toMonoidWithZeroHom ≍ toMonoidWithZeroHom' → P) → P

Defined in

Mathlib.Algebra.Order.Hom.MonoidWithZero

Cited by

1 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms