Theorems · Definition · general topology
Filter.EventuallyConst
{α : Type u_1} → {β : Type u_2} → (α → β) → Filter α → PropThe proposition that a function is eventually constant along a filter on the domain.
- Defined in
- Mathlib.Order.Filter.EventuallyConst
- Cited by
- 93 results in Mathlib
- Foundations
- Depth 10 from the axioms, rests on 28 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Filterstatement and proof · cited by 8,121
- Filter.mapproof · cited by 819
- Filter.Subsingletonproof · cited by 15
Cited by99
Results whose statement or proof uses this declaration.
- Filter.EventuallyConst.compstatement and proof · cited by 8
- PreErgodic.aeconst_setstatement · cited by 7
- aeconst_of_dense_setOfPred_preimage_smul_aestatement · cited by 4
- aeconst_of_dense_setOfPred_preimage_vadd_aestatement · cited by 4
- Filter.eventuallyConst_preimagestatement · cited by 4
- Filter.EventuallyConst.of_monotone_of_lt_cofstatement · cited by 3
- aeconst_of_dense_setOfPred_preimage_smul_eqstatement · cited by 3
- aeconst_of_dense_setOfPred_preimage_vadd_eqstatement · cited by 3
- Filter.EventuallyConst.comp₂statement and proof · cited by 3
- Filter.eventuallyConst_atTopstatement · cited by 3
- Filter.eventuallyConst_set'statement · cited by 3
- Filter.eventuallyConst_iff_exists_eventuallyEqstatement · cited by 3