Theorems · Theorem · order theory

LatticeHom.mk.inj

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

Defined in

Mathlib.Order.Hom.Lattice

Cited by

1 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms