Commit 2023-08-22 13:23 896b6feb

View on Github →

refactor(Filter/EventuallyConst): redefine (#6673)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Order/Filter/EventuallyConst.lean

modified theorem Filter.EventuallyConst.comp

deleted theorem Filter.EventuallyConst.mono

added theorem Filter.EventuallyConst.mulIndicator_const

added theorem Filter.EventuallyConst.mulIndicator_const_iff

added theorem Filter.EventuallyConst.mulIndicator_const_iff_of_ne

modified theorem Filter.EventuallyConst.of_mulIndicator_const

deleted theorem Filter.EventuallyConst.of_subsingleton

added theorem Filter.EventuallyConst.of_subsingleton_left

added theorem Filter.EventuallyConst.of_subsingleton_right

added theorem Filter.EventuallyConst.of_tendsto

deleted theorem Filter.EventuallyConst.of_unique

modified def Filter.EventuallyConst

modified theorem Filter.EventuallyEq.eventuallyConst_iff

added theorem Filter.HasBasis.eventuallyConst_iff'

added theorem Filter.HasBasis.eventuallyConst_iff

added theorem Filter.eventuallyConst_id

added theorem Filter.eventuallyConst_iff_exists_eventuallyEq

modified theorem Filter.eventuallyConst_iff_tendsto

Created Mathlib/Order/Filter/Subsingleton.lean

added theorem Filter.HasBasis.subsingleton_iff

added theorem Filter.Subsingleton.anti

added theorem Filter.Subsingleton.exists_eq_pure

added theorem Filter.Subsingleton.map

added theorem Filter.Subsingleton.of_subsingleton

added theorem Filter.Subsingleton.prod

added theorem Filter.subsingleton_bot

added theorem Filter.subsingleton_iff_bot_or_pure

added theorem Filter.subsingleton_iff_exists_le_pure

added theorem Filter.subsingleton_iff_exists_singleton_mem

added theorem Filter.subsingleton_pure