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`.
