mathlib
32cd2787
- feat(analysis/asymptotics): add a few lemmas (#11623)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
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`.
Author
urkud
Parents
095c46c2
Loading