Commit 2024-10-21 18:56 c3f00b0c

View on Github →

feat(Analysis/SpecificLimits/Basic): add lemmas about limits of fractions (#16768) Used in #15373.

Estimated changes

Modified Mathlib/Analysis/SpecificLimits/Basic.lean

added theorem Filter.EventuallyEq.div_mul_cancel

added theorem Filter.EventuallyEq.div_mul_cancel_atTop

added theorem Tendsto.den

added theorem Tendsto.num

added theorem Tendsto.num_atTop_iff_den_atTop

added theorem tendsto_mod_div_atTop_nhds_zero_nat

Modified Mathlib/Data/Set/Pointwise/Interval.lean

added theorem Set.preimage_const_mul_Ioi_or_Iio

Modified Mathlib/Topology/Algebra/Order/Field.lean

added theorem bdd_le_mul_tendsto_zero'

added theorem bdd_le_mul_tendsto_zero

added theorem tendsto_bdd_div_atTop_nhds_zero