Theorems · Theorem · order theory

SupBotHom.sup_apply

∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β]
  (f g : SupBotHom α β) (a : α), (f ⊔ g) a = f a ⊔ g a

Defined in

Mathlib.Order.Hom.BoundedLattice

Cited by

0 results in Mathlib

Foundations

Depth 14 from the axioms · uses propext

Assumes

MaxBotSemilatticeSupOrderBot