Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-04 15:24 dc95d02e

View on Github →

feat(order/filter/archimedean): add lemmas about convergence to ±∞ for archimedean rings / groups. (#12427) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/order/filter/archimedean.lean

added theorem filter.tendsto.at_bot_mul_const'

added theorem filter.tendsto.at_bot_mul_neg_const'

added theorem filter.tendsto.at_bot_zsmul_const

added theorem filter.tendsto.at_bot_zsmul_neg_const

modified theorem filter.tendsto.at_top_mul_const'

added theorem filter.tendsto.at_top_mul_neg_const'

added theorem filter.tendsto.at_top_nsmul_const

added theorem filter.tendsto.at_top_nsmul_neg_const

added theorem filter.tendsto.at_top_zsmul_const

added theorem filter.tendsto.at_top_zsmul_neg_const

modified theorem filter.tendsto.const_mul_at_top'

Modified src/order/filter/at_top_bot.lean

added theorem filter.tendsto_at_bot_iff_tends_to_neg_at_top

added theorem filter.tendsto_at_top_iff_tends_to_neg_at_bot