Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-16 12:55 a8c10e1c

View on Github →

chore(topology/algebra/ordered): rename lim*_eq_of_tendsto to tendsto.lim*_eq (#3415) Also add tendsto_of_le_liminf_of_limsup_le

Estimated changes

Modified src/analysis/analytic/basic.lean

Modified src/measure_theory/integration.lean

Modified src/topology/algebra/ordered.lean

added theorem filter.tendsto.liminf_eq

added theorem filter.tendsto.limsup_eq

deleted theorem liminf_eq_of_tendsto

deleted theorem limsup_eq_of_tendsto

added theorem tendsto_of_le_liminf_of_limsup_le