Theorems · Theorem · order theory

CompleteLatticeHom.mk.injEq

∀ {α : Type u_8} {β : Type u_9} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (tosInfHom : sInfHom α β)
  (map_sSup' : ∀ (s : Set α), tosInfHom.toFun (sSup s) = sSup (tosInfHom.toFun '' s)) (tosInfHom_1 : sInfHom α β)
  (map_sSup'_1 : ∀ (s : Set α), tosInfHom_1.toFun (sSup s) = sSup (tosInfHom_1.toFun '' s)),
  ({ tosInfHom := tosInfHom, map_sSup' := map_sSup' } = { tosInfHom := tosInfHom_1, map_sSup' := map_sSup'_1 }) =
    (tosInfHom = tosInfHom_1)

Defined in

Mathlib.Order.Hom.CompleteLattice

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

CompleteLatticeCompleteLattice