Commit 2025-07-10 16:28 80ef7ee0

View on Github →

chore(Order/Filter/Basic): rename EventuallyLE.le_iff_eq to EventuallyLE.ge_iff_eq' (#26969)

Estimated changes

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.EventuallyLE.ge_iff_eq'

deleted theorem Filter.EventuallyLE.le_iff_eq