Commit 2024-11-22 02:00 43c93172

View on Github →

chore(Topology/Order): rename 2 lemmas (#19261) ... to allow dot notation.

Estimated changes

Modified Mathlib/Algebra/Order/Floor/Prime.lean

Modified Mathlib/Analysis/Asymptotics/TVS.lean

Modified Mathlib/Analysis/BoundedVariation.lean

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

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

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Computability/AkraBazzi/AkraBazzi.lean

Modified Mathlib/Data/Real/Pi/Irrational.lean

Modified Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean

Modified Mathlib/MeasureTheory/Function/LpSpace.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/MeasureTheory/Measure/WithDensity.lean

Modified Mathlib/Topology/Order/IntermediateValue.lean

Modified Mathlib/Topology/Order/OrderClosed.lean

added theorem Filter.Tendsto.eventually_const_le

added theorem Filter.Tendsto.eventually_const_lt

added theorem Filter.Tendsto.eventually_le_const

added theorem Filter.Tendsto.eventually_lt_const

deleted theorem eventually_ge_of_tendsto_gt

deleted theorem eventually_gt_of_tendsto_gt

deleted theorem eventually_le_of_tendsto_lt

deleted theorem eventually_lt_of_tendsto_lt