Commit 2025-03-03 16:46 6141bf3c

View on Github →

chore(Topology,Analysis): rename some lemmas (#22486)

Estimated changes

Modified Mathlib/Analysis/Calculus/DSlope.lean

added theorem dslope_eventuallyEq_slope_nhdsNE

deleted theorem dslope_eventuallyEq_slope_punctured_nhds

Modified Mathlib/Analysis/Calculus/Deriv/Inverse.lean

added theorem HasDerivAt.tendsto_nhdsNE

deleted theorem HasDerivAt.tendsto_punctured_nhds

Modified Mathlib/Analysis/Calculus/LHopital.lean

deleted theorem HasDerivAt.lhopital_zero_nhds'

added theorem HasDerivAt.lhopital_zero_nhdsGT

added theorem HasDerivAt.lhopital_zero_nhdsLT

added theorem HasDerivAt.lhopital_zero_nhdsNE

deleted theorem HasDerivAt.lhopital_zero_nhds_left

deleted theorem HasDerivAt.lhopital_zero_nhds_right

deleted theorem deriv.lhopital_zero_nhds'

added theorem deriv.lhopital_zero_nhdsGT

added theorem deriv.lhopital_zero_nhdsLT

added theorem deriv.lhopital_zero_nhdsNE

deleted theorem deriv.lhopital_zero_nhds_left

deleted theorem deriv.lhopital_zero_nhds_right

Modified Mathlib/Analysis/Convex/Gauge.lean

deleted theorem tendsto_gauge_nhds_zero'

added theorem tendsto_gauge_nhds_zero_nhdsGE

Modified Mathlib/Analysis/LocallyConvex/Basic.lean

added theorem absorbent_iff_eventually_nhdsNE_zero

deleted theorem absorbent_iff_eventually_nhdsWithin_zero

added theorem absorbs_iff_eventually_nhdsNE_zero

deleted theorem absorbs_iff_eventually_nhdsWithin_zero

Modified Mathlib/Analysis/Normed/Field/Basic.lean

added theorem NormedField.nhdsNE_neBot

deleted theorem NormedField.punctured_nhds_neBot

Modified Mathlib/Analysis/Seminorm.lean

Modified Mathlib/Analysis/SpecialFunctions/Integrals.lean

Modified Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean

Modified Mathlib/Analysis/SpecialFunctions/NonIntegrable.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

added theorem isLittleO_abs_log_rpow_rpow_nhdsGT_zero

deleted theorem isLittleO_abs_log_rpow_rpow_nhds_zero

added theorem isLittleO_log_rpow_nhdsGT_zero

deleted theorem isLittleO_log_rpow_nhds_zero

added theorem tendsto_log_div_rpow_nhdsGT_zero

deleted theorem tendsto_log_div_rpow_nhds_zero

added theorem tendsto_log_mul_rpow_nhdsGT_zero

deleted theorem tendsto_log_mul_rpow_nhds_zero

added theorem tendsto_log_mul_self_nhdsLT_zero

deleted theorem tendsto_log_mul_self_nhds_zero_left

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/ComplexDeriv.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/Topology/Compactification/OnePoint.lean

added theorem OnePoint.nhdsNE_infty_eq

deleted theorem OnePoint.nhdsWithin_compl_infty_eq

Modified Mathlib/Topology/ContinuousOn.lean

added theorem nhdsNE_sup_pure

deleted theorem nhdsWithin_compl_singleton_sup_pure

added theorem pure_sup_nhdsNE