Mathlib v3 is deprecated. Go to Mathlib v4

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_leis_bounded_mono;
  • is_bounded_under_of_is_boundedis_bounded.is_bounded_under;
  • is_cobounded_of_is_boundedis_bounded.is_cobounded_flip;
  • is_cobounded_of_leis_cobounded.mono;

Top namespace

  • is_bounded_under_le_of_tendstofilter.tendsto.is_bounded_under_le;
  • is_cobounded_under_ge_of_tendstofilter.tendsto.is_cobounded_under_ge;
  • is_bounded_under_ge_of_tendstofilter.tendsto.is_bounded_under_ge;
  • is_cobounded_under_le_of_tendstofilter.tendsto.is_cobounded_under_le.

Remove

  • filter.is_trans_le, filter.is_trans_ge: we have both in order/rel_classes.

Estimated changes