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.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

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.

theorem countable_sInter_mem {α : Type u_2} {l : Filter α} [CountableInterFilter l] {S : Set (Set α)} (hSc : S.Countable) : ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l

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

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

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

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

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

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

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

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

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

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

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

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

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 := ⋯ }

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 (Filter.ofCountableInter l hl h_mono)

Equations

• ⋯ = ⋯

@[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 ∈ Filter.ofCountableInter l hl h_mono ↔ s ∈ l

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} ⋯ ⋯

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 (Filter.ofCountableUnion l h₁ h₂)

Equations

• ⋯ = ⋯

@[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 ∈ Filter.ofCountableUnion l hunion hmono ↔ l sᶜ

instance countableInterFilter_principal {α : Type u_2} (s : Set α) : CountableInterFilter (Filter.principal s)

Equations

• ⋯ = ⋯

instance countableInterFilter_bot {α : Type u_2} : CountableInterFilter ⊥

Equations

• ⋯ = ⋯

instance countableInterFilter_top {α : Type u_2} : CountableInterFilter ⊤

Equations

• ⋯ = ⋯

instance instCountableInterFilterComap {α : Type u_2} {β : Type u_3} (l : Filter β) [CountableInterFilter l] (f : α → β) : CountableInterFilter (Filter.comap f l)

Equations

• ⋯ = ⋯

instance instCountableInterFilterMap {α : Type u_2} {β : Type u_3} (l : Filter α) [CountableInterFilter l] (f : α → β) : CountableInterFilter (Filter.map f l)

Equations

• ⋯ = ⋯

instance countableInterFilter_inf {α : Type u_2} (l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] : CountableInterFilter (l₁ ⊓ l₂)

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

Equations

• ⋯ = ⋯

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

Supremum of two CountableInterFilters is a CountableInterFilter.

Equations

• ⋯ = ⋯

instance CountableInterFilter.curry {α : Type u_4} {β : Type u_5} {l : Filter α} {m : Filter β} [CountableInterFilter l] [CountableInterFilter m] : CountableInterFilter (l.curry m)

Equations

• ⋯ = ⋯

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 → Filter.CountableGenerateSets g s
• univ: ∀ {α : Type u_2} {g : Set (Set α)}, Filter.CountableGenerateSets g Set.univ
• superset: ∀ {α : Type u_2} {g : Set (Set α)} {s t : Set α}, Filter.CountableGenerateSets g s → s ⊆ t → Filter.CountableGenerateSets g t
• sInter: ∀ {α : Type u_2} {g S : Set (Set α)}, S.Countable → (∀ s ∈ S, Filter.CountableGenerateSets g s) → Filter.CountableGenerateSets g (⋂₀ S)

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) ⋯ ⋯

instance Filter.instCountableInterFilterCountableGenerate {α : Type u_2} (g : Set (Set α)) : CountableInterFilter (Filter.countableGenerate g)

Equations

• ⋯ = ⋯

theorem Filter.mem_countableGenerate_iff {α : Type u_2} {g : Set (Set α)} {s : Set α} : s ∈ Filter.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.

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

theorem Filter.countableGenerate_isGreatest {α : Type u_2} (g : Set (Set α)) : IsGreatest {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets} (Filter.countableGenerate g)

countableGenerate g is the greatest countableInterFilter containing g.