Commit 2025-01-06 22:50 ac937eec

View on Github →

feat(Analysis): asymptotics of inversion at atBot and 𝓝[<] 0 (#19817) Prove some lemmas about the inversion function's asymptotics at atBot and 𝓝[<] 0 filters, analogous to the existing API for atTop and 𝓝[>] 0

Estimated changes

Modified Mathlib/Algebra/Order/Group/Pointwise/Interval.lean

added theorem Set.inv_Iio₀

added theorem Set.inv_Ioo_0_right

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

added theorem Filter.Tendsto.const_div_atBot

added theorem Filter.Tendsto.div_atBot

added theorem Filter.Tendsto.inv_tendsto_atBot

added theorem Filter.Tendsto.inv_tendsto_nhdsLT_zero

added theorem inv_atBot₀

added theorem inv_nhdsLT_zero

added theorem tendsto_inv_atBot_zero'

added theorem tendsto_inv_atBot_zero

added theorem tendsto_inv_zero_atBot