Commit 2020-07-26 09:05 f95e90b4
View on Github →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 inorder/rel_classes
.