Theorems · Definition · order theory

LatticeHom.mk.noConfusion

{α : Type u_6} →
  {β : Type u_7} →
    {inst : Lattice α} →
      {inst_1 : Lattice β} →
        {P : Sort u} →
          {toSupHom : SupHom α β} →
            {map_inf' : ∀ (a b : α), toSupHom.toFun (a ⊓ b) = toSupHom.toFun a ⊓ toSupHom.toFun b} →
              {toSupHom' : SupHom α β} →
                {map_inf'' : ∀ (a b : α), toSupHom'.toFun (a ⊓ b) = toSupHom'.toFun a ⊓ toSupHom'.toFun b} →
                  { toSupHom := toSupHom, map_inf' := map_inf' } = { toSupHom := toSupHom', map_inf' := map_inf'' } →
                    (toSupHom ≍ toSupHom' → P) → P

Defined in

Mathlib.Order.Hom.Lattice

Cited by

1 results in Mathlib

Foundations

Depth 9 from the axioms · uses no axioms