Commit 2021-08-02 12:31 f354c1b1

feat(order/bounded_lattice): add some disjoint lemmas (#8407) This adds disjoint.inf_left and disjoint.inf_right (and primed variants) to match the existing disjoint.sup_left and disjoint.sup_right. This also duplicates these lemmas to use set notation with inter instead of inf, matching the existing disjoint.union_left and disjoint.union_right.