Structures · Order
CountableInterFilter
A filter l has the countable intersection property if for any countable collection
of sets s ∈ l their intersection belongs to l as well.
- Defined in
- Mathlib.Order.Filter.CountableInter
- Shape
- One type argument · adds countable_sInter_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances1
- Prod
How is a type an instance?
Loading the hierarchy index…
Assumed by77
- eventually_countable_forall
- countable_sInter_mem
- EventuallyMeasurable
- eventually_le_limsup
- countable_bInter_mem
- EventuallyMeasurableSet
- ENNReal.eventually_le_limsup
- Filter.EventuallyEq.countable_iUnion
- ENNReal.limsup_const_mul
- Filter.EventuallyLE.countable_iUnion
- EventuallyMeasurableSet.congr
- MeasurableSet.eventuallyMeasurableSet
- Filter.EventuallyLE.countable_iInter
- countable_iInter_mem
- eventually_countable_ball
- limsup_eq_bot
- Filter.exists_subset_subsingleton_mem_of_forall_separating
- Filter.EventuallyEq.countable_bInter
- Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating
- Filter.EventuallyEq.countable_bUnion
- Filter.EventuallyEq.of_forall_eventually_lt_iff
- Filter.EventuallyLE.countable_bInter
- Measurable.eventuallyMeasurable
- Filter.exists_singleton_mem_of_mem_of_forall_separating
- EventuallyMeasurable.congr
- Filter.EventuallyEq.of_forall_separating_preimage
- IsLindelof.compl_mem_sets_of_nhdsWithin
- Filter.EventuallyLE.countable_bUnion
- Filter.le_countableGenerate_iff_of_countableInterFilter
- Filter.EventuallyEq.of_eventually_mem_of_forall_separating_mem_iff
- eventually_le_const_iff_forall_gt_eventually_lt_const
- Filter.EventuallyEq.of_eventually_mem_of_forall_separating_preimage
- Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating
- le_eventuallyMeasurableSpace
- Filter.exists_singleton_mem_of_forall_separating
- ENNReal.limsup_add_le
- ENNReal.limsup_eq_zero_iff
- Filter.exists_eventuallyEq_const_of_forall_separating
- eventuallyMeasurableSpace
- ENNReal.limsup_mul_le
- eventuallyMeasurableSet_of_mem_filter
- IsLindelof.compl_mem_sets
- Measurable.comp_eventuallyMeasurable
- IsLindelof.disjoint_nhdsSet_left
- Filter.EventuallyEq.of_forall_eventually_le_iff
- eventually_liminf_le
- Filter.EventuallyEq.countable_iInter
- CountableInterFilter.countable_sInter_mem
- ENNReal.limsup_liminf_le_liminf_limsup
- Filter.EventuallyEq.of_forall_eventually_gt_iff
Ancestors0
No ancestors.