mathlib
22b7d21f - feat(analysis/normed): if `f → 0` and `g` is bounded, then `f g → 0` (#13248)

Commit

3 years ago

feat(analysis/normed*): if `f → 0` and `g` is bounded, then `f * g → 0` (#13248) Also drop `is_bounded_under_of_tendsto`: it's just `h.norm.is_bounded_under_le`.

Author

urkud

Parents

4c4e5e83

mathlib 22b7d21f - feat(analysis/normed*): if `f → 0` and `g` is bounded, then `f * g → 0` (#13248)

mathlib
22b7d21f - feat(analysis/normed): if `f → 0` and `g` is bounded, then `f g → 0` (#13248)