Commit 2020-05-07 15:51 5d3b8307

refactor(order/lattice): add sup/inf_eq_*, rename inf_le_inf_* (#2624)

New lemmas:

• sup_eq_right : a ⊔ b = b ↔a ≤ b, and similarly for sup_eq_left, left_eq_sup, right_eq_sup, inf_eq_right, inf_eq_left, left_eq_inf, and right_eq_inf; all these lemmas are @[simp];
• sup_elim and inf_elim: if (≤) is a total order, then p a → p b → p (a ⊔ b), and similarly for inf.

Renamed

• inf_le_inf_right is now inf_le_inf_left and vice versa. This agrees with sup_le_sup_left/sup_le_sup_right, and the rest of the library.
• ord_continuous_sup -> ord_continuous.sup;
• ord_continuous_mono -> ord_continuous.mono.