Theorems · Definition · category theory

BddDistLat.ofHom

{X Y : Type u} →
  [inst : DistribLattice X] →
    [inst_1 : BoundedOrder X] →
      [inst_2 : DistribLattice Y] →
        [inst_3 : BoundedOrder Y] → BoundedLatticeHom X Y → (BddDistLat.of X ⟶ BddDistLat.of Y)

Typecheck a BoundedLatticeHom as a morphism in BddDistLat.

Defined in

Mathlib.Order.Category.BddDistLat

Cited by

9 results in Mathlib

Foundations

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

Assumes

DistribLatticeBoundedOrderDistribLatticeBoundedOrder