mathlib

fd6f6816 - feat(order/bounded_lattice): add `is_compl.le_sup_right_iff_inf_left_le` (#10014)

feat(order/bounded_lattice): add `is_compl.le_sup_right_iff_inf_left_le` (#10014) This lemma is a generalization of `is_compl.inf_left_eq_bot_iff`. Also drop `inf_eq_bot_iff_le_compl` in favor of `is_compl.inf_left_eq_bot_iff` and add `set.subset_union_compl_iff_inter_subset`.