Commit 2023-09-04 15:04 7a05698b

View on Github →

feat: x ↦ x / a tendsto to infinity in ℕ (#6914) and a few lemmas missing from Order.Filter.AtTopBot.

Estimated changes

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

added theorem Nat.tendsto_div_const_atTop

Modified Mathlib/Order/Filter/AtTopBot.lean

added theorem Filter.tendsto_div_const_atTop_iff_pos

added theorem Filter.tendsto_div_const_atTop_of_pos