proposition: Lemma join_ub_l : forall x y : X, x <= join x y.
proof: Proof. Proof (sl_meet_lb_l _ _ (l_proof X)). Lemma join_ub_r : forall x y : X, y <= join x y. Proof (sl_meet_lb_r _ _ (l_proof X)). Lemma join_lub : forall x y z : X, x <= z -> y <= z -> join x y <= z. Proof (sl_meet_glb _ _ (l_proof X)). Definition Dual : Lattice := @makeLattice (Dual X) (@join X) (@meet X) join_ub_l join_ub_r join_lub (@meet_lb_l X) (@meet_lb_r X) (@meet_glb X). Lemma join_comm : forall x y:X, join x y == join y x. Proof meet_comm Dual. Lemma join_assoc : forall x y z:X, join x (join y z) == join (join x y) z. Proof meet_assoc Dual. Lemma join_idem : forall x:X, join x x == x. Proof meet_idem Dual. Lemma le_join_l : forall x y : X, y <= x <-> join x y == x. Proof le_meet_l Dual. Lemma le_join_r : forall x y : X, x <= y <-> join x y == y. Proof le_meet_r Dual. Lemma join_monotone_r : forall a : X, monotone X (join a). Proof meet_monotone_r Dual. Lemma join_monotone_l : forall a : X, monotone X (fun x => join x a). Proof meet_monotone_l Dual. Lemma join_le_compat : forall w x y z : X, w<=y -> x<=z -> join w x <= join y z. Proof fun w x y z => meet_le_compat Dual y z w x. End Join. Add Parametric Morphism X : (@join X) with signature (@st_eq (sl X)) ==> (@st_eq X) ==> (@st_eq X) as join_compat. Proof. exact (meet_compat (Dual X)). Qed.
imports: Coq.Setoids.Setoid CoRN.order.SemiLattice