Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-01-24 03:52 32cd2787

View on Github →

feat(analysis/asymptotics): add a few lemmas (#11623)

  • rename is_o.tendsto_0 to is_o.tendsto_div_nhds_zero, add is_o.tendsto_inv_smul_nhds_zero;
  • add is_o_const_left and filter.is_bounded_under.is_o_sub_self_inv.

Estimated changes