Theorems · Theorem · order theory

FrameHom.mk.injEq

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

Defined in

Mathlib.Order.Hom.CompleteLattice

Cited by

0 results in Mathlib

Foundations

Depth 16 from the axioms · uses propext

Assumes

CompleteLatticeCompleteLattice