Commit 2020-07-26 09:05 f95e90b4

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.