Theorems · Theorem · order theory

FrameHom.mk.congr_simp

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

Defined in

Mathlib.Order.Category.Frm

Cited by

0 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

CompleteLatticeCompleteLattice