EventuallyConst

📁 Source: Mathlib/Order/Filter/EventuallyConst.lean

Statistics

Metric	Count
Definitions `EventuallyConst`	1
Theorems `add`, `anti`, `apply`, `bot`, `comp`, `comp_tendsto`, `comp₂`, `const`, `eventuallyEq_const`, `exists_tendsto`, `indicator_const`, `indicator_const_iff`, `indicator_const_iff_of_ne`, `inv`, `mul`, `mulIndicator_const`, `mulIndicator_const_iff`, `mulIndicator_const_iff_of_ne`, `neg`, `of_indicator_const`, `of_mulIndicator_const`, `of_subsingleton_left`, `of_subsingleton_right`, `of_tendsto`, `prodMk`, `eventuallyConst_iff`, `eventuallyConst_iff`, `eventuallyConst_iff'`, `eventuallyConst_atTop`, `eventuallyConst_atTop_nat`, `eventuallyConst_id`, `eventuallyConst_iff_exists_eventuallyEq`, `eventuallyConst_iff_tendsto`, `eventuallyConst_pred`, `eventuallyConst_pred'`, `eventuallyConst_preimage`, `eventuallyConst_set`, `eventuallyConst_set'`	38
Total	39

Filter

Definitions

Name	Category	Theorems
`EventuallyConst` 📖	MathDef	50 math math: `aeconst_of_dense_aestabilizer_smul`, `eventuallyConst_atTop`, `EventuallyConst.indicator_const_iff`, `IsArtinian.eventuallyConst_of_isArtinian`, `EventuallyConst.bot`, `MeasureTheory.eventuallyConst_inv_set_ae`, `EventuallyEq.eventuallyConst_iff`, `MeasureTheory.eventuallyConst_smul_set_ae`, `HasBasis.eventuallyConst_iff'`, `MulAction.aeconst_of_aestabilizer_eq_top`, `EventuallyConst.const`, `EventuallyConst.of_subsingleton_left`, `ErgodicVAdd.aeconst_of_forall_preimage_vadd_ae_eq`, `aeconst_of_dense_setOf_preimage_smul_eq`, `eventuallyConst_set`, `eventuallyConst_set'`, `eventuallyConst_atTop_nat`, `EventuallyConst.mulIndicator_const_iff`, `ergodicSMul_iff`, `HasBasis.eventuallyConst_iff`, `aeconst_of_dense_aestabilizer_vadd`, `MeasureTheory.aeconst_of_forall_preimage_smul_ae_eq`, `aeconst_of_dense_setOf_preimage_vadd_eq`, `eventuallyConst_iff_exists_eventuallyEq`, `eventuallyConst_iff_tendsto`, `QuasiErgodic.aeconst_set₀`, `ErgodicSMul.aeconst_of_forall_preimage_smul_ae_eq`, `ergodicVAdd_iff`, `EventuallyConst.of_subsingleton_right`, `eventuallyConst_id`, `EventuallyConst.indicator_const_iff_of_ne`, `aeconst_of_dense_setOf_preimage_vadd_ae`, `MeasureTheory.MeasurePreserving.aeconst_preimage`, `MeasureTheory.MeasurePreserving.aeconst_comp`, `eventuallyConst_preimage`, `MeasureTheory.aeconst_of_forall_vadd_ae_eq`, `eventuallyConst_nhdsNE_iff_meromorphicOrderAt_sub_eq_top`, `MeasureTheory.aeconst_of_forall_smul_ae_eq`, `eventuallyConst_of_isNoetherian`, `eventuallyConst_iff_analyticOrderAt_sub_eq_top`, `aeconst_of_dense_setOf_preimage_smul_ae`, `AddAction.aeconst_of_aestabilizer_eq_top`, `MeasureTheory.eventuallyConst_neg_set_ae`, `eventuallyConst_pred`, `EventuallyConst.mulIndicator_const_iff_of_ne`, `MeasureTheory.eventuallyConst_vadd_set_ae`, `EventuallyConst.of_tendsto`, `PreErgodic.aeconst_set`, `MeasureTheory.aeconst_of_forall_preimage_vadd_ae_eq`, `eventuallyConst_pred'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyConst_atTop` 📖	mathematical	—	`EventuallyConst` `atTop` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder`	—	`HasBasis.eventuallyConst_iff'` `atTop_basis` `SemilatticeSup.instIsDirectedOrder` `Set.self_mem_Ici`
`eventuallyConst_atTop_nat` 📖	mathematical	—	`EventuallyConst` `atTop` `Nat.instPreorder`	—	`eventuallyConst_atTop` `LE.le.trans` `Nat.le_induction`
`eventuallyConst_id` 📖	mathematical	—	`EventuallyConst` `Subsingleton`	—	—
`eventuallyConst_iff_exists_eventuallyEq` 📖	mathematical	—	`EventuallyConst` `EventuallyEq`	—	`subsingleton_iff_exists_singleton_mem`
`eventuallyConst_iff_tendsto` 📖	mathematical	—	`EventuallyConst` `Tendsto` `Filter` `instPure`	—	`subsingleton_iff_exists_le_pure`
`eventuallyConst_pred` 📖	mathematical	—	`EventuallyConst` `Eventually`	—	—
`eventuallyConst_pred'` 📖	mathematical	—	`EventuallyConst` `EventuallyEq`	—	—
`eventuallyConst_preimage` 📖	mathematical	—	`EventuallyConst` `Set.preimage` `map`	—	—
`eventuallyConst_set` 📖	mathematical	—	`EventuallyConst` `Eventually` `Set` `Set.instMembership`	—	`eventuallyConst_pred`
`eventuallyConst_set'` 📖	mathematical	—	`EventuallyConst` `EventuallyEq` `Set` `Set.instEmptyCollection` `Set.univ`	—	`eventuallyConst_pred'`

Filter.EventuallyConst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add` 📖	mathematical	`Filter.EventuallyConst`	`Pi.instAdd`	—	`comp₂`
`anti` 📖	—	`Filter.EventuallyConst` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder`	—	—	`Filter.Subsingleton.anti` `Filter.map_mono`
`apply` 📖	—	`Filter.EventuallyConst`	—	—	`comp`
`bot` 📖	mathematical	—	`Filter.EventuallyConst` `Bot.bot` `Filter` `Filter.instBot`	—	`Filter.subsingleton_bot`
`comp` 📖	—	`Filter.EventuallyConst`	—	—	`Filter.Subsingleton.map`
`comp_tendsto` 📖	—	`Filter.EventuallyConst` `Filter.Tendsto`	—	—	`anti`
`comp₂` 📖	—	`Filter.EventuallyConst`	—	—	`Filter.Subsingleton.anti` `Filter.Subsingleton.map` `Filter.Subsingleton.prod` `Filter.Tendsto.comp` `Filter.tendsto_map` `Filter.Tendsto.prodMk`
`const` 📖	mathematical	—	`Filter.EventuallyConst`	—	`of_tendsto` `Filter.tendsto_const_pure`
`eventuallyEq_const` 📖	mathematical	`Filter.EventuallyConst`	`Filter.EventuallyEq`	—	`Filter.eventuallyConst_iff_exists_eventuallyEq`
`exists_tendsto` 📖	mathematical	`Filter.EventuallyConst`	`Filter.Tendsto` `Filter` `Filter.instPure`	—	`Filter.eventuallyConst_iff_tendsto`
`indicator_const` 📖	mathematical	`Filter.EventuallyConst`	`Set.indicator`	—	`comp`
`indicator_const_iff` 📖	mathematical	—	`Filter.EventuallyConst` `Set.indicator`	—	`eq_or_ne` `Set.indicator_zero` `const` `indicator_const_iff_of_ne`
`indicator_const_iff_of_ne` 📖	mathematical	—	`Filter.EventuallyConst` `Set.indicator`	—	`of_indicator_const` `indicator_const`
`inv` 📖	mathematical	`Filter.EventuallyConst`	`Pi.instInv`	—	`comp`
`mul` 📖	mathematical	`Filter.EventuallyConst`	`Pi.instMul`	—	`comp₂`
`mulIndicator_const` 📖	mathematical	`Filter.EventuallyConst`	`Set.mulIndicator`	—	`comp`
`mulIndicator_const_iff` 📖	mathematical	—	`Filter.EventuallyConst` `Set.mulIndicator`	—	`eq_or_ne` `Set.mulIndicator_one`
`mulIndicator_const_iff_of_ne` 📖	mathematical	—	`Filter.EventuallyConst` `Set.mulIndicator`	—	`of_mulIndicator_const` `mulIndicator_const`
`neg` 📖	mathematical	`Filter.EventuallyConst`	`Pi.instNeg`	—	`comp`
`of_indicator_const` 📖	—	`Filter.EventuallyConst` `Set.indicator`	—	—	`Set.indicator_apply_eq_self` `comp`
`of_mulIndicator_const` 📖	—	`Filter.EventuallyConst` `Set.mulIndicator`	—	—	`comp`
`of_subsingleton_left` 📖	mathematical	—	`Filter.EventuallyConst`	—	`Filter.Subsingleton.map` `Filter.Subsingleton.of_subsingleton`
`of_subsingleton_right` 📖	mathematical	—	`Filter.EventuallyConst`	—	`Filter.Subsingleton.of_subsingleton`
`of_tendsto` 📖	mathematical	`Filter.Tendsto` `Filter` `Filter.instPure`	`Filter.EventuallyConst`	—	`Filter.eventuallyConst_iff_tendsto`
`prodMk` 📖	—	`Filter.EventuallyConst`	—	—	`comp₂`

Filter.EventuallyEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyConst_iff` 📖	mathematical	`Filter.EventuallyEq`	`Filter.EventuallyConst`	—	`Filter.map_congr`

Filter.HasBasis

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventuallyConst_iff` 📖	mathematical	`Filter.HasBasis`	`Filter.EventuallyConst`	—	`subsingleton_iff` `map`
`eventuallyConst_iff'` 📖	mathematical	`Filter.HasBasis` `Set` `Set.instMembership`	`Filter.EventuallyConst`	—	`eventuallyConst_iff`

---

← Back to Index