mathlib

f95e90b4 - chore(order/liminf_limsup): use dot notation and `order_dual` (#3555)

chore(order/liminf_limsup): use dot notation and `order_dual` (#3555) ## New * `filter.has_basis.Limsup_eq_infi_Sup` ## Rename ### Namespace `filter` * `is_bounded_of_le` → `is_bounded_mono`; * `is_bounded_under_of_is_bounded` → `is_bounded.is_bounded_under`; * `is_cobounded_of_is_bounded` → `is_bounded.is_cobounded_flip`; * `is_cobounded_of_le` → `is_cobounded.mono`; ### Top namespace * `is_bounded_under_le_of_tendsto` → `filter.tendsto.is_bounded_under_le`; * `is_cobounded_under_ge_of_tendsto` → `filter.tendsto.is_cobounded_under_ge`; * `is_bounded_under_ge_of_tendsto` → `filter.tendsto.is_bounded_under_ge`; * `is_cobounded_under_le_of_tendsto` → `filter.tendsto.is_cobounded_under_le`. ## Remove * `filter.is_trans_le`, `filter.is_trans_ge`: we have both in `order/rel_classes`.