Theorems · Definition · category theory

BoolAlg.ofHom

{X Y : Type u} →
  [inst : BooleanAlgebra X] →
    [inst_1 : BooleanAlgebra Y] →
      BoundedLatticeHom X Y → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })

Typecheck a BoundedLatticeHom as a morphism in BoolAlg.

Defined in

Mathlib.Order.Category.BoolAlg

Cited by

14 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

BooleanAlgebraBooleanAlgebra