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∈ l their intersection belongs to l as well.

Two main examples are the residual filter defined in Mathlib.Topology.MetricSpace.Baire and the measure.ae filter defined in measure_theory.measure_space.

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_1} (l : Filter α) :

For a countable collection of sets s ∈ l∈ l, their intersection belongs to l as well.
countable_interₛ_mem : ∀ (S : Set (Set α)), Set.Countable S → (∀ (s : Set α), s ∈ S → s ∈ l) → ⋂₀ S ∈ l

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

Instances

theorem countable_interₛ_mem {α : Type u_1} {l : Filter α} [inst : CountableInterFilter l] {S : Set (Set α)} (hSc : Set.Countable S) :

⋂₀ S ∈ l ↔ ∀ (s : Set α), s ∈ S → s ∈ l

theorem countable_interᵢ_mem {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ι → Set α} :

(Set.interᵢ fun i => s i) ∈ l ↔ ∀ (i : ι), s i ∈ l

theorem countable_bInter_mem {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i ∈ S → Set α} :

(Set.interᵢ fun i => Set.interᵢ fun hi => s i hi) ∈ l ↔ ∀ (i : ι) (hi : i ∈ S), s i hi ∈ l

theorem eventually_countable_forall {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {p : α → ι → Prop} :

Filter.Eventually (fun x => (i : ι) → p x i) l ↔ ∀ (i : ι), Filter.Eventually (fun x => p x i) l

theorem eventually_countable_ball {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {p : α → (i : ι) → i ∈ S → Prop} :

Filter.Eventually (fun x => (i : ι) → (hi : i ∈ S) → p x i hi) l ↔ ∀ (i : ι) (hi : i ∈ S), Filter.Eventually (fun x => p x i hi) l

theorem EventuallyLE.countable_unionᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :

(Set.unionᵢ fun i => s i) ≤ᶠ[l] Set.unionᵢ fun i => t i

theorem EventuallyEq.countable_unionᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :

(Set.unionᵢ fun i => s i) =ᶠ[l] Set.unionᵢ fun i => t i

theorem EventuallyLE.countable_bUnion {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i ∈ S → Set α} {t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) :

(Set.unionᵢ fun i => Set.unionᵢ fun h => s i h) ≤ᶠ[l] Set.unionᵢ fun i => Set.unionᵢ fun h => t i h

theorem EventuallyEq.countable_bUnion {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i ∈ S → Set α} {t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) :

(Set.unionᵢ fun i => Set.unionᵢ fun h => s i h) =ᶠ[l] Set.unionᵢ fun i => Set.unionᵢ fun h => t i h

theorem EventuallyLE.countable_interᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :

(Set.interᵢ fun i => s i) ≤ᶠ[l] Set.interᵢ fun i => t i

theorem EventuallyEq.countable_interᵢ {ι : Sort u_1} {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] [inst : Countable ι] {s : ι → Set α} {t : ι → Set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :

(Set.interᵢ fun i => s i) =ᶠ[l] Set.interᵢ fun i => t i

theorem EventuallyLE.countable_bInter {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i ∈ S → Set α} {t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi) :

(Set.interᵢ fun i => Set.interᵢ fun h => s i h) ≤ᶠ[l] Set.interᵢ fun i => Set.interᵢ fun h => t i h

theorem EventuallyEq.countable_bInter {α : Type u_2} {l : Filter α} [inst : CountableInterFilter l] {ι : Type u_1} {S : Set ι} (hS : Set.Countable S) {s : (i : ι) → i ∈ S → Set α} {t : (i : ι) → i ∈ S → Set α} (h : ∀ (i : ι) (hi : i ∈ S), s i hi =ᶠ[l] t i hi) :

(Set.interᵢ fun i => Set.interᵢ fun h => s i h) =ᶠ[l] Set.interᵢ fun i => Set.interᵢ fun h => t i h

def Filter.ofCountableInter {α : Type u_1} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) :

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

Equations

One or more equations did not get rendered due to their size.

instance Filter.countable_Inter_ofCountableInter {α : Type u_1} (l : Set (Set α)) (hp : ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) :

CountableInterFilter (Filter.ofCountableInter l hp h_mono)

Equations

@Filter.countable_Inter_ofCountableInter = @Filter.countable_Inter_ofCountableInter.proof_1

@[simp]

theorem Filter.mem_ofCountableInter {α : Type u_1} {l : Set (Set α)} (hp : ∀ (S : Set (Set α)), Set.Countable S → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l) {s : Set α} :

s ∈ Filter.ofCountableInter l hp h_mono ↔ s ∈ l

instance countableInterFilter_principal {α : Type u_1} (s : Set α) :

CountableInterFilter (Filter.principal s)

Equations

@countableInterFilter_principal = @countableInterFilter_principal.proof_1

instance countableInterFilter_bot {α : Type u_1} :

CountableInterFilter ⊥

Equations

@countableInterFilter_bot = @countableInterFilter_bot.proof_1

instance countableInterFilter_top {α : Type u_1} :

CountableInterFilter ⊤

Equations

@countableInterFilter_top = @countableInterFilter_top.proof_1

instance instCountableInterFilterComap {α : Type u_1} {β : Type u_2} (l : Filter β) [inst : CountableInterFilter l] (f : α → β) :

CountableInterFilter (Filter.comap f l)

Equations

@instCountableInterFilterComap = @instCountableInterFilterComap.proof_1

instance instCountableInterFilterMap {α : Type u_1} {β : Type u_2} (l : Filter α) [inst : CountableInterFilter l] (f : α → β) :

CountableInterFilter (Filter.map f l)

Equations

@instCountableInterFilterMap = @instCountableInterFilterMap.proof_1

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

CountableInterFilter (l₁ ⊓ l₂)

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

Equations

@countableInterFilter_inf = @countableInterFilter_inf.proof_1

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

CountableInterFilter (l₁ ⊔ l₂)

Supremum of two countable_Inter_filters is a countable_Inter_filter.

Equations

@countableInterFilter_sup = @countableInterFilter_sup.proof_1