Commit 2021-10-28 17:00 fd6f6816
View on Github →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.