# Documentation

Mathlib.Order.Filter.CountableInter

# Filters with countable intersection property #

In this file we define CountableInterFilter to be the class of filters with the following property: for any countable collection of sets s ∈ l their intersection belongs to l as well.

Two main examples are the residual filter defined in Mathlib.Topology.GDelta and the MeasureTheory.Measure.ae filter defined in MeasureTheory.MeasureSpace.

We reformulate the definition in terms of indexed intersection and in terms of Filter.Eventually and provide instances for some basic constructions (⊥, ⊤, Filter.principal, Filter.map, Filter.comap, Inf.inf). We also provide a custom constructor Filter.ofCountableInter that deduces two axioms of a Filter from the countable intersection property.

## Tags #

filter, countable

class CountableInterFilter {α : Type u_2} (l : ) :
• countable_sInter_mem : ∀ (S : Set (Set α)), (∀ (s : Set α), s Ss l) → ⋂₀ S l

For a countable collection of sets s ∈ l, their intersection belongs to l as well.

A filter l has the countable intersection property if for any countable collection of sets s ∈ l their intersection belongs to l as well.

Instances
theorem countable_sInter_mem {α : Type u_2} {l : } {S : Set (Set α)} (hSc : ) :
⋂₀ S l ∀ (s : Set α), s Ss l
theorem countable_iInter_mem {ι : Sort u_1} {α : Type u_2} {l : } [] {s : ιSet α} :
⋂ (i : ι), s i l ∀ (i : ι), s i l
theorem countable_bInter_mem {α : Type u_2} {l : } {ι : Type u_4} {S : Set ι} (hS : ) {s : (i : ι) → i SSet α} :
⋂ (i : ι) (hi : i S), s i hi l ∀ (i : ι) (hi : i S), s i hi l
theorem eventually_countable_forall {ι : Sort u_1} {α : Type u_2} {l : } [] {p : αιProp} :
(∀ᶠ (x : α) in l, (i : ι) → p x i) ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
theorem eventually_countable_ball {α : Type u_2} {l : } {ι : Type u_4} {S : Set ι} (hS : ) {p : α(i : ι) → i SProp} :
(∀ᶠ (x : α) in l, (i : ι) → (hi : i S) → p x i hi) ∀ (i : ι) (hi : i S), ∀ᶠ (x : α) in l, p x i hi
theorem EventuallyLE.countable_iUnion {ι : Sort u_1} {α : Type u_2} {l : } [] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i
theorem EventuallyEq.countable_iUnion {ι : Sort u_1} {α : Type u_2} {l : } [] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i
theorem EventuallyLE.countable_bUnion {α : Type u_2} {l : } {ι : Type u_4} {S : Set ι} (hS : ) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi ≤ᶠ[l] t i hi) :
⋃ (i : ι) (h : i S), s i h ≤ᶠ[l] ⋃ (i : ι) (h : i S), t i h
theorem EventuallyEq.countable_bUnion {α : Type u_2} {l : } {ι : Type u_4} {S : Set ι} (hS : ) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi =ᶠ[l] t i hi) :
⋃ (i : ι) (h : i S), s i h =ᶠ[l] ⋃ (i : ι) (h : i S), t i h
theorem EventuallyLE.countable_iInter {ι : Sort u_1} {α : Type u_2} {l : } [] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i
theorem EventuallyEq.countable_iInter {ι : Sort u_1} {α : Type u_2} {l : } [] {s : ιSet α} {t : ιSet α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i
theorem EventuallyLE.countable_bInter {α : Type u_2} {l : } {ι : Type u_4} {S : Set ι} (hS : ) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi ≤ᶠ[l] t i hi) :
⋂ (i : ι) (h : i S), s i h ≤ᶠ[l] ⋂ (i : ι) (h : i S), t i h
theorem EventuallyEq.countable_bInter {α : Type u_2} {l : } {ι : Type u_4} {S : Set ι} (hS : ) {s : (i : ι) → i SSet α} {t : (i : ι) → i SSet α} (h : ∀ (i : ι) (hi : i S), s i hi =ᶠ[l] t i hi) :
⋂ (i : ι) (h : i S), s i h =ᶠ[l] ⋂ (i : ι) (h : i S), t i h
def Filter.ofCountableInter {α : Type u_2} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), S l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) :

Construct a filter with countable intersection property. This constructor deduces Filter.univ_sets and Filter.inter_sets from the countable intersection property.

Instances For
instance Filter.countable_Inter_ofCountableInter {α : Type u_2} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), S l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) :
@[simp]
theorem Filter.mem_ofCountableInter {α : Type u_2} {l : Set (Set α)} (hp : ∀ (S : Set (Set α)), S l⋂₀ S l) (h_mono : ∀ (s t : Set α), s ls tt l) {s : Set α} :
instance countableInterFilter_principal {α : Type u_2} (s : Set α) :
instance countableInterFilter_bot {α : Type u_2} :
instance countableInterFilter_top {α : Type u_2} :
instance instCountableInterFilterComap {α : Type u_2} {β : Type u_3} (l : ) (f : αβ) :
instance instCountableInterFilterMap {α : Type u_2} {β : Type u_3} (l : ) (f : αβ) :
instance countableInterFilter_inf {α : Type u_2} (l₁ : ) (l₂ : ) [] [] :

Infimum of two CountableInterFilters is a CountableInterFilter. This is useful, e.g., to automatically get an instance for residual α ⊓ 𝓟 s.

instance countableInterFilter_sup {α : Type u_2} (l₁ : ) (l₂ : ) [] [] :

Supremum of two CountableInterFilters is a CountableInterFilter.

inductive Filter.CountableGenerateSets {α : Type u_2} (g : Set (Set α)) :
Set αProp

Filter.CountableGenerateSets g is the (sets of the) greatest countableInterFilter containing g.

Instances For
def Filter.countableGenerate {α : Type u_2} (g : Set (Set α)) :

Filter.countableGenerate g is the greatest countableInterFilter containing g.

Instances For
theorem Filter.mem_countableGenerate_iff {α : Type u_2} {g : Set (Set α)} {s : Set α} :
S, S g ⋂₀ S s

A set is in the countableInterFilter generated by g if and only if it contains a countable intersection of elements of g.

theorem Filter.le_countableGenerate_iff_of_countableInterFilter {α : Type u_2} {g : Set (Set α)} {f : } :
g f.sets
theorem Filter.countableGenerate_isGreatest {α : Type u_2} (g : Set (Set α)) :
IsGreatest {f | g f.sets} ()

countableGenerate g is the greatest countableInterFilter containing g.