Commit 2023-03-02 10:20 5d9a516c

View on Github →

chore: rename Filter.EventuallyLe (#2464)

Estimated changes

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.EventuallyLE.antisymm

added theorem Filter.EventuallyLE.compl

added theorem Filter.EventuallyLE.congr

added theorem Filter.EventuallyLE.diff

added theorem Filter.EventuallyLE.inter

added theorem Filter.EventuallyLE.le_iff_eq

added theorem Filter.EventuallyLE.le_sup_of_le_left

added theorem Filter.EventuallyLE.le_sup_of_le_right

added theorem Filter.EventuallyLE.mul_le_mul'

added theorem Filter.EventuallyLE.mul_le_mul

added theorem Filter.EventuallyLE.mul_nonneg

added theorem Filter.EventuallyLE.refl

added theorem Filter.EventuallyLE.rfl

added theorem Filter.EventuallyLE.sup

added theorem Filter.EventuallyLE.sup_le

added theorem Filter.EventuallyLE.trans

added theorem Filter.EventuallyLE.trans_eq

added theorem Filter.EventuallyLE.union

added def Filter.EventuallyLE

deleted theorem Filter.EventuallyLe.antisymm

deleted theorem Filter.EventuallyLe.compl

deleted theorem Filter.EventuallyLe.congr

deleted theorem Filter.EventuallyLe.diff

deleted theorem Filter.EventuallyLe.inter

deleted theorem Filter.EventuallyLe.le_iff_eq

deleted theorem Filter.EventuallyLe.le_sup_of_le_left

deleted theorem Filter.EventuallyLe.le_sup_of_le_right

deleted theorem Filter.EventuallyLe.mul_le_mul'

deleted theorem Filter.EventuallyLe.mul_le_mul

deleted theorem Filter.EventuallyLe.mul_nonneg

deleted theorem Filter.EventuallyLe.refl

deleted theorem Filter.EventuallyLe.rfl

deleted theorem Filter.EventuallyLe.sup

deleted theorem Filter.EventuallyLe.sup_le

deleted theorem Filter.EventuallyLe.trans

deleted theorem Filter.EventuallyLe.trans_eq

deleted theorem Filter.EventuallyLe.union

deleted def Filter.EventuallyLe

added theorem Filter.eventuallyLE_antisymm_iff

added theorem Filter.eventuallyLE_bind

added theorem Filter.eventuallyLE_congr

deleted theorem Filter.eventuallyLe_antisymm_iff

deleted theorem Filter.eventuallyLe_bind

deleted theorem Filter.eventuallyLe_congr

added theorem HasSubset.Subset.eventuallyLE

deleted theorem HasSubset.Subset.eventuallyLe

Modified Mathlib/Order/Filter/CountableInter.lean

added theorem EventuallyLE.countable_bInter

added theorem EventuallyLE.countable_bUnion

added theorem EventuallyLE.countable_interᵢ

added theorem EventuallyLE.countable_unionᵢ

deleted theorem EventuallyLe.countable_bInter

deleted theorem EventuallyLe.countable_bUnion

deleted theorem EventuallyLe.countable_interᵢ

deleted theorem EventuallyLe.countable_unionᵢ

Modified Mathlib/Order/Filter/ENNReal.lean

Modified Mathlib/Order/Filter/Extr.lean

added theorem Filter.EventuallyLE.isMaxFilter

added theorem Filter.EventuallyLE.isMinFilter

deleted theorem Filter.EventuallyLe.isMaxFilter

deleted theorem Filter.EventuallyLe.isMinFilter

Modified Mathlib/Order/Filter/FilterProduct.lean

Modified Mathlib/Order/Filter/Germ.lean

Modified Mathlib/Order/Filter/IndicatorFunction.lean

added theorem indicator_eventuallyLE_indicator

deleted theorem indicator_eventuallyLe_indicator

Modified Mathlib/Order/Filter/Prod.lean

added theorem Filter.EventuallyLE.prod_map

deleted theorem Filter.EventuallyLe.prod_map

Modified Mathlib/Topology/Basic.lean

added theorem Filter.EventuallyLE.eventuallyLE_nhds

deleted theorem Filter.EventuallyLe.eventuallyLe_nhds

added theorem eventually_eventuallyLE_nhds

deleted theorem eventually_eventuallyLe_nhds

Modified Mathlib/Topology/LocalExtr.lean

added theorem Filter.EventuallyLE.isLocalMax

added theorem Filter.EventuallyLE.isLocalMaxOn

added theorem Filter.EventuallyLE.isLocalMin

added theorem Filter.EventuallyLE.isLocalMinOn

deleted theorem Filter.EventuallyLe.isLocalMax

deleted theorem Filter.EventuallyLe.isLocalMaxOn

deleted theorem Filter.EventuallyLe.isLocalMin

deleted theorem Filter.EventuallyLe.isLocalMinOn

Modified Mathlib/Topology/Order/Basic.lean