Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-12 15:28 b6a47633

View on Github →

refactor(order/filter): replace tendsto_comp_succ_at_top_iff by tendsto_add_at_top_iff_nat

Estimated changes

Modified src/analysis/specific_limits.lean

deleted theorem tendsto_comp_succ_at_top_iff

modified theorem tendsto_one_div_add_at_top_nhds_0_nat

modified theorem tendsto_pow_at_top_at_top_of_gt_1_nat

Modified src/order/filter/basic.lean

added theorem filter.tendsto_add_at_top_iff_nat

Modified src/topology/metric_space/lipschitz.lean