# 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.lean` and the `MeasureTheory.ae` filter defined in `Mathlib/MeasureTheory.OuterMeasure/AE`.

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.

Note that there also exists a typeclass `CardinalInterFilter`, and thus an alternative spelling of `CountableInterFilter` as `CardinalInterFilter l ℵ₁`. The former (defined here) is the preferred spelling; it has the advantage of not requiring the user to import the theory of ordinals.

## Tags #

filter, countable

source
class CountableInterFilter {α : Type u_2} (l : Filter α) :
Prop

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

- countable_sInter_mem (S : Set (Set α)) : S.Countable → (∀ s ∈ S, s ∈ l) → ⋂₀ S ∈ l

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

Instances

source
theorem countable_sInter_mem {α : Type u_2} {l : Filter α} [CountableInterFilter l] {S : Set (Set α)} (hSc : S.Countable) :
⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l
source
theorem countable_iInter_mem {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s : ι → Set α} :
⋂ (i : ι), s i ∈ l ↔ ∀ (i : ι), s i ∈ l
source
theorem countable_bInter_mem {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : S.Countable) {s : (i : ι) → i ∈ S → Set α} :
⋂ (i : ι), ⋂ (hi : i ∈ S), s i hi ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l
source
theorem eventually_countable_forall {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {p : α → ι → Prop} :
(∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
source
theorem eventually_countable_ball {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : S.Countable) {p : α → (i : ι) → i ∈ S → Prop} :
(∀ᶠ (x : α) in l, ∀ (i : ι) (hi : i ∈ S), p x i hi) ↔ ∀ (i : ι) (hi : i ∈ S), ∀ᶠ (x : α) in l, p x i hi
source
theorem EventuallyLE.countable_iUnion {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋃ (i : ι), s i ≤ᶠ[l] ⋃ (i : ι), t i
source
theorem EventuallyEq.countable_iUnion {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋃ (i : ι), s i =ᶠ[l] ⋃ (i : ι), t i
source
theorem EventuallyLE.countable_bUnion {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : S.Countable) {s t : (i : ι) → i ∈ S → Set α} (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
source
theorem EventuallyEq.countable_bUnion {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : S.Countable) {s t : (i : ι) → i ∈ S → Set α} (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
source
theorem EventuallyLE.countable_iInter {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
⋂ (i : ι), s i ≤ᶠ[l] ⋂ (i : ι), t i
source
theorem EventuallyEq.countable_iInter {ι : Sort u_1} {α : Type u_2} {l : Filter α} [CountableInterFilter l] [Countable ι] {s t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
⋂ (i : ι), s i =ᶠ[l] ⋂ (i : ι), t i
source
theorem EventuallyLE.countable_bInter {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : S.Countable) {s t : (i : ι) → i ∈ S → Set α} (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
source
theorem EventuallyEq.countable_bInter {α : Type u_2} {l : Filter α} [CountableInterFilter l] {ι : Type u_4} {S : Set ι} (hS : S.Countable) {s t : (i : ι) → i ∈ S → Set α} (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
source
def Filter.ofCountableInter {α : Type u_2} (l : Set (Set α)) (hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) :
Filter α

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

Equations

- Filter.ofCountableInter l hl h_mono = { sets := l, univ_sets := ⋯, sets_of_superset := ⋯, inter_sets := ⋯ }

Instances For

source
instance Filter.countableInter_ofCountableInter {α : Type u_2} (l : Set (Set α)) (hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) :
CountableInterFilter (ofCountableInter l hl h_mono)
source
@[simp]
theorem Filter.mem_ofCountableInter {α : Type u_2} {l : Set (Set α)} (hl : ∀ (S : Set (Set α)), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) {s : Set α} :
s ∈ ofCountableInter l hl h_mono ↔ s ∈ l
source
def Filter.ofCountableUnion {α : Type u_2} (l : Set (Set α)) (hUnion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) (hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) :
Filter α

Construct a filter with countable intersection property. Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property. Similarly to `Filter.ofCountableInter`, this constructor deduces some properties from the countable intersection property which becomes the countable union property because we take complements of all sets.

Equations

- Filter.ofCountableUnion l hUnion hmono = Filter.ofCountableInter {s : Set α | s ᶜ ∈ l} ⋯ ⋯

Instances For

source
instance Filter.countableInter_ofCountableUnion {α : Type u_2} (l : Set (Set α)) (h₁ : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) (h₂ : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) :
CountableInterFilter (ofCountableUnion l h₁ h₂)
source
@[simp]
theorem Filter.mem_ofCountableUnion {α : Type u_2} {l : Set (Set α)} {hunion : ∀ (S : Set (Set α)), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l} {hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l} {s : Set α} :
s ∈ ofCountableUnion l hunion hmono ↔ l s ᶜ
source
instance countableInterFilter_principal {α : Type u_2} (s : Set α) :
CountableInterFilter (Filter.principal s)
source
instance countableInterFilter_bot {α : Type u_2} :
CountableInterFilter ⊥
source
instance countableInterFilter_top {α : Type u_2} :
CountableInterFilter ⊤
source
instance instCountableInterFilterComap {α : Type u_2} {β : Type u_3} (l : Filter β) [CountableInterFilter l] (f : α → β) :
CountableInterFilter (Filter.comap f l)
source
instance instCountableInterFilterMap {α : Type u_2} {β : Type u_3} (l : Filter α) [CountableInterFilter l] (f : α → β) :
CountableInterFilter (Filter.map f l)
source
instance countableInterFilter_inf {α : Type u_2} (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] :
CountableInterFilter (l₁ ⊓ l₂)

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

source
instance countableInterFilter_sup {α : Type u_2} (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] :
CountableInterFilter (l₁ ⊔ l₂)

Supremum of two `CountableInterFilter`s is a `CountableInterFilter`.

source
instance CountableInterFilter.curry {α : Type u_4} {β : Type u_5} {l : Filter α} {m : Filter β} [CountableInterFilter l] [CountableInterFilter m] :
CountableInterFilter (l.curry m)
source
inductive Filter.CountableGenerateSets {α : Type u_2} (g : Set (Set α)) :
Set α → Prop

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

- basic {α : Type u_2} {g : Set (Set α)} {s : Set α} : s ∈ g → CountableGenerateSets g s
- univ {α : Type u_2} {g : Set (Set α)} : CountableGenerateSets g Set.univ
- superset {α : Type u_2} {g : Set (Set α)} {s t : Set α} : CountableGenerateSets g s → s ⊆ t → CountableGenerateSets g t
- sInter {α : Type u_2} {g S : Set (Set α)} : S.Countable → (∀ s ∈ S, CountableGenerateSets g s) → CountableGenerateSets g (⋂₀ S)

Instances For

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

`Filter.countableGenerate g` is the greatest `countableInterFilter` containing `g`.

Equations

- Filter.countableGenerate g = Filter.ofCountableInter (Filter.CountableGenerateSets g) ⋯ ⋯

Instances For

source
instance Filter.instCountableInterFilterCountableGenerate {α : Type u_1} (g : Set (Set α)) :
CountableInterFilter (countableGenerate g)
Equations

- ⋯ = ⋯

source
theorem Filter.mem_countableGenerate_iff {α : Type u_2} {g : Set (Set α)} {s : Set α} :
s ∈ countableGenerate g ↔ ∃ S ⊆ g, S.Countable ∧ ⋂₀ S ⊆ s

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

source
theorem Filter.le_countableGenerate_iff_of_countableInterFilter {α : Type u_2} {g : Set (Set α)} {f : Filter α} [CountableInterFilter f] :
f ≤ countableGenerate g ↔ g ⊆ f.sets
source
theorem Filter.countableGenerate_isGreatest {α : Type u_2} (g : Set (Set α)) :
IsGreatest {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)

`countableGenerate g` is the greatest `countableInterFilter` containing `g`.