CoRN.model.lattice.CRlattice
Definition CRLattice : Lattice :=
makeLattice CRPartialOrder (ucFun2 CRmin) (ucFun2 CRmax)
CRmin_lb_l CRmin_lb_r CRmin_glb CRmax_ub_l CRmax_ub_r CRmax_lub.
Section CRLattice.
Let CRlat := CRLattice.
Open Local Scope CR_scope.
Definition CRmin_comm : ∀ x y : CR, CRmin x y == CRmin y x := @meet_comm CRlat.
Definition CRmin_assoc : ∀ x y z : CR, CRmin x (CRmin y z) == CRmin (CRmin x y) z:=
@meet_assoc CRlat.
Definition CRmin_idem : ∀ x : CR, CRmin x x == x := @meet_idem CRlat.
Definition CRle_min_l : ∀ x y : CR, x ≤ y ↔ CRmin x y == x := @le_meet_l CRlat.
Definition CRle_min_r : ∀ x y : CR, y ≤ x ↔ CRmin x y == y := @le_meet_r CRlat.
Definition CRmin_monotone_r : ∀ a : CR, CRmonotone (CRmin a) :=
@meet_monotone_r CRlat.
Definition CRmin_monotone_l : ∀ a : CR, CRmonotone (fun x ⇒ CRmin x a) :=
@meet_monotone_l CRlat.
Definition CRmin_le_compat :
∀ w x y z : CR, w ≤ y → x ≤ z → CRmin w x ≤ CRmin y z :=
@meet_le_compat CRlat.
Definition CRmax_comm : ∀ x y : CR, CRmax x y == CRmax y x := @join_comm CRlat.
Definition CRmax_assoc : ∀ x y z : CR, CRmax x (CRmax y z) == CRmax (CRmax x y) z:=
@join_assoc CRlat.
Definition CRmax_idem : ∀ x : CR, CRmax x x == x := @join_idem CRlat.
Definition CRle_max_l : ∀ x y : CR, y ≤ x ↔ CRmax x y == x := @le_join_l CRlat.
Definition CRle_max_r : ∀ x y : CR, x ≤ y ↔ CRmax x y == y := @le_join_r CRlat.
Definition CRmax_monotone_r : ∀ a : CR, CRmonotone (CRmax a) :=
@join_monotone_r CRlat.
Definition CRmax_monotone_l : ∀ a : CR, CRmonotone (fun x ⇒ CRmax x a) :=
@join_monotone_l CRlat.
Definition CRmax_le_compat :
∀ w x y z : CR, w≤y → x≤z → CRmax w x ≤ CRmax y z :=
@join_le_compat CRlat.
Definition CRmin_max_absorb_l_l : ∀ x y : CR, CRmin x (CRmax x y) == x :=
@meet_join_absorb_l_l CRlat.
Definition CRmax_min_absorb_l_l : ∀ x y : CR, CRmax x (CRmin x y) == x :=
@join_meet_absorb_l_l CRlat.
Definition CRmin_max_absorb_l_r : ∀ x y : CR, CRmin x (CRmax y x) == x :=
@meet_join_absorb_l_r CRlat.
Definition CRmax_min_absorb_l_r : ∀ x y : CR, CRmax x (CRmin y x) == x :=
@join_meet_absorb_l_r CRlat.
Definition CRmin_max_absorb_r_l : ∀ x y : CR, CRmin (CRmax x y) x == x :=
@meet_join_absorb_r_l CRlat.
Definition CRmax_min_absorb_r_l : ∀ x y : CR, CRmax (CRmin x y) x == x :=
@join_meet_absorb_r_l CRlat.
Definition CRmin_max_absorb_r_r : ∀ x y : CR, CRmin (CRmax y x) x == x :=
@meet_join_absorb_r_r CRlat.
Definition CRmax_min_absorb_r_r : ∀ x y : CR, CRmax (CRmin y x) x == x :=
@join_meet_absorb_r_r CRlat.
Definition CRmin_max_eq : ∀ x y : CR, CRmin x y == CRmax x y → x == y :=
@meet_join_eq CRlat.
End CRLattice.