Skip to main content

MeetSemilattice

typeclass S: MeetSemilattice extends PartialOrder, Meet {
    meet_lte_left(a: S, b: S) {
        a.meet(b) <= a
    }
    meet_lte_right(a: S, b: S) {
        a.meet(b) <= b
    }
    lte_meet_of_bounds(c: S, a: S, b: S) {
        c <= a and c <= b implies c <= a.meet(b)
    }
}

A partially ordered type with binary greatest lower bounds.

GitHub

antisymmetric​

Inherited from PartialOrder.

gt​

Inherited from PartialOrder.

gte​

Inherited from PartialOrder.

lt​

Inherited from PartialOrder.

lte​

Inherited from LTE.

lte_meet_of_bounds​

lte_meet_of_bounds(c: S, a: S, b: S) {
    c <= a and c <= b implies c <= a.meet(b)
}

Any common lower bound is below the meet.

meet​

Inherited from Meet.

meet_lte_left​

meet_lte_left(a: S, b: S) {
    a.meet(b) <= a
}

A meet is below its left argument.

meet_lte_right​

meet_lte_right(a: S, b: S) {
    a.meet(b) <= b
}

A meet is below its right argument.

reflexive​

Inherited from PartialOrder.

transitive​

Inherited from PartialOrder.