Commit 2022-06-06 20:46 2b7e72b0

feat(order/liminf_limsup): add a few lemmas (#14554)

• add is_bounded_under.mono_le, is_bounded_under.mono_ge;
• add order_iso.is_bounded_under_le_comp, order_iso.is_bounded_under_ge_comp;
• add is_bounded_under_le_inv, is_bounded_under_le_inv, and additive versions;
• rename is_bounded_under_sup and is_bounded_under_inf to is_bounded_under.sup and is_bounded_under.inf;
• add iff versions under names is_bounded_under_le_sup and is_bounded_under_ge_inf;
• add is_bounded_under_le_abs.