Theorems · Theorem · order theory

SupBotHom.coe_mk

∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : Max β] [inst_3 : Bot β] (f : SupHom α β)
  (hf : f.toFun ⊥ = ⊥), ⇑{ toSupHom := f, map_bot' := hf } = ⇑f

Defined in

Mathlib.Order.Hom.BoundedLattice

Cited by

1 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

MaxBotMaxBot