Theorems · Theorem · order theory

FrameHom.mk.inj

∀ {α : 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

1 results in Mathlib

Foundations

Depth 15 from the axioms · uses no axioms