Commit 2023-06-19 16:31 0c4c62b4

View on Github →

feat: functions eventually constant along filters (#5248) Heavily based on the code from the sphere eversion project.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Logic/Basic.lean

added theorem Prop.exists_iff

added theorem Prop.forall_iff

Created Mathlib/Order/Filter/EventuallyConst.lean

added theorem Filter.EventuallyConst.apply

added theorem Filter.EventuallyConst.comp

added theorem Filter.EventuallyConst.comp_tendsto

added theorem Filter.EventuallyConst.comp₂

added theorem Filter.EventuallyConst.mono

added theorem Filter.EventuallyConst.mul

added theorem Filter.EventuallyConst.of_mulIndicator_const

added theorem Filter.EventuallyConst.of_subsingleton

added theorem Filter.EventuallyConst.of_unique

added theorem Filter.EventuallyConst.prod_mk

added def Filter.EventuallyConst

added theorem Filter.eventuallyConst_atTop

added theorem Filter.eventuallyConst_atTop_nat

added theorem Filter.eventuallyConst_iff_tendsto

added theorem Filter.eventuallyConst_pred'

added theorem Filter.eventuallyConst_pred

added theorem Filter.eventuallyConst_set'

added theorem Filter.eventuallyConst_set