fact: Record is_SemiLattice (po : PartialOrder) (meet : po -> po -> po) : Prop := { sl_meet_lb_l : forall x y, meet x y <= x ; sl_meet_lb_r : forall x y, meet x y <= y ; sl_meet_glb : forall x y z, z <= x -> z <= y -> z <= meet x y }.
imports: CoRN.order.PartialOrder