Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nnreal.tendsto_cofinite_zero_of_summable

Modification history

2021-02-08 14:15
src/topology/instances/nnreal.lean
feat(topology/instances/{nnreal,ennreal}): add tendsto_cofinite_zero_of_summable (#6093) …
Added nnreal.tendsto_cofinite_zero_of_summableView on Github →