Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-29 21:31 c14c84e4

View on Github →

chore(topology/algebra/ordered): le_of_tendsto: use ∀ᶠ, add primed versions (#2270) Also fix two typos in order/filter/basic

Estimated changes

Modified src/analysis/normed_space/basic.lean

Modified src/measure_theory/decomposition.lean

Modified src/measure_theory/l1_space.lean

Modified src/order/filter/basic.lean

deleted theorem filter.tendso_add_at_top_nat

deleted theorem filter.tendso_sub_at_top_nat

added theorem filter.tendsto_add_at_top_nat

added theorem filter.tendsto_sub_at_top_nat

Modified src/topology/algebra/infinite_sum.lean

Modified src/topology/algebra/ordered.lean

added theorem ge_of_tendsto'

added theorem le_of_tendsto'

added theorem le_of_tendsto_of_tendsto'

Modified src/topology/bounded_continuous_function.lean