mathlib3 documentation

order.filter.countable_Inter

Filters with countable intersection property #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define countable_Inter_filter 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 topology.G_delta 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, has_inf.inf). We also provide a custom constructor filter.of_countable_Inter that deduces two axioms of a filter from the countable intersection property.

Tags #

filter, countable

source
@[class]
structure countable_Inter_filter {α : 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.

Instances of this typeclass
source
theorem countable_sInter_mem {α : Type u_2} {l : filter α} [countable_Inter_filter l] {S : set (set α)} (hSc : S.countable) :
⋂₀ S ∈ l ↔ ∀ (s : set α), s ∈ S → s ∈ l
source
theorem countable_Inter_mem {ι : Sort u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [countable ι] {s : ι → set α} :
(⋂ (i : ι), s i) ∈ l ↔ ∀ (i : ι), s i ∈ l
source
theorem countable_bInter_mem {α : Type u_2} {l : filter α} [countable_Inter_filter l] {ι : Type u_1} {S : set ι} (hS : S.countable) {s : Π (i : ι), i ∈ S → set α} :
(⋂ (i : ι) (H : i ∈ S), s i H) ∈ l ↔ ∀ (i : ι) (H : i ∈ S), s i H ∈ l
source
theorem eventually_countable_forall {ι : Sort u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter 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 α} [countable_Inter_filter l] {ι : Type u_1} {S : set ι} (hS : S.countable) {p : α → Π (i : ι), i ∈ S → Prop} :
(∀ᶠ (x : α) in l, ∀ (i : ι) (H : i ∈ S), p x i H) ↔ ∀ (i : ι) (H : i ∈ S), ∀ᶠ (x : α) in l, p x i H
source
theorem eventually_le.countable_Union {ι : Sort u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [countable ι] {s t : ι → set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
(⋃ (i : ι), s i) ≤ᶠ[l] ⋃ (i : ι), t i
source
theorem eventually_eq.countable_Union {ι : Sort u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [countable ι] {s t : ι → set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
(⋃ (i : ι), s i) =ᶠ[l] ⋃ (i : ι), t i
source
theorem eventually_le.countable_bUnion {α : Type u_2} {l : filter α} [countable_Inter_filter l] {ι : Type u_1} {S : set ι} (hS : S.countable) {s t : Π (i : ι), i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), s i H ≤ᶠ[l] t i H) :
(⋃ (i : ι) (H : i ∈ S), s i H) ≤ᶠ[l] ⋃ (i : ι) (H : i ∈ S), t i H
source
theorem eventually_eq.countable_bUnion {α : Type u_2} {l : filter α} [countable_Inter_filter l] {ι : Type u_1} {S : set ι} (hS : S.countable) {s t : Π (i : ι), i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), s i H =ᶠ[l] t i H) :
(⋃ (i : ι) (H : i ∈ S), s i H) =ᶠ[l] ⋃ (i : ι) (H : i ∈ S), t i H
source
theorem eventually_le.countable_Inter {ι : Sort u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [countable ι] {s t : ι → set α} (h : ∀ (i : ι), s i ≤ᶠ[l] t i) :
(⋂ (i : ι), s i) ≤ᶠ[l] ⋂ (i : ι), t i
source
theorem eventually_eq.countable_Inter {ι : Sort u_1} {α : Type u_2} {l : filter α} [countable_Inter_filter l] [countable ι] {s t : ι → set α} (h : ∀ (i : ι), s i =ᶠ[l] t i) :
(⋂ (i : ι), s i) =ᶠ[l] ⋂ (i : ι), t i
source
theorem eventually_le.countable_bInter {α : Type u_2} {l : filter α} [countable_Inter_filter l] {ι : Type u_1} {S : set ι} (hS : S.countable) {s t : Π (i : ι), i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), s i H ≤ᶠ[l] t i H) :
(⋂ (i : ι) (H : i ∈ S), s i H) ≤ᶠ[l] ⋂ (i : ι) (H : i ∈ S), t i H
source
theorem eventually_eq.countable_bInter {α : Type u_2} {l : filter α} [countable_Inter_filter l] {ι : Type u_1} {S : set ι} (hS : S.countable) {s t : Π (i : ι), i ∈ S → set α} (h : ∀ (i : ι) (H : i ∈ S), s i H =ᶠ[l] t i H) :
(⋂ (i : ι) (H : i ∈ S), s i H) =ᶠ[l] ⋂ (i : ι) (H : i ∈ S), t i H
source
def filter.of_countable_Inter {α : Type u_2} (l : set (set α)) (hp : ∀ (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
Instances for filter.of_countable_Inter
source
@[protected, instance]
def filter.countable_Inter_of_countable_Inter {α : Type u_2} (l : set (set α)) (hp : ∀ (S : set (set α)), S.countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : set α), s ∈ l → s ⊆ t → t ∈ l) :
countable_Inter_filter (filter.of_countable_Inter l hp h_mono)
source
@[simp]
theorem filter.mem_of_countable_Inter {α : Type u_2} {l : set (set α)} (hp : ∀ (S : set (set α)), S.countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ (s t : set α), s ∈ l → s ⊆ t → t ∈ l) {s : set α} :
s ∈ filter.of_countable_Inter l hp h_mono ↔ s ∈ l
source
@[protected, instance]
def countable_Inter_filter_principal {α : Type u_2} (s : set α) :
countable_Inter_filter (filter.principal s)
source
@[protected, instance]
def countable_Inter_filter_bot {α : Type u_2} :
countable_Inter_filter ⊥
source
@[protected, instance]
def countable_Inter_filter_top {α : Type u_2} :
countable_Inter_filter ⊤
source
@[protected, instance]
def filter.comap.countable_Inter_filter {α : Type u_2} {β : Type u_3} (l : filter β) [countable_Inter_filter l] (f : α → β) :
countable_Inter_filter (filter.comap f l)
source
@[protected, instance]
def filter.map.countable_Inter_filter {α : Type u_2} {β : Type u_3} (l : filter α) [countable_Inter_filter l] (f : α → β) :
countable_Inter_filter (filter.map f l)
source
@[protected, instance]
def countable_Inter_filter_inf {α : Type u_2} (l₁ l₂ : filter α) [countable_Inter_filter l₁] [countable_Inter_filter l₂] :
countable_Inter_filter (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.

source
@[protected, instance]
def countable_Inter_filter_sup {α : Type u_2} (l₁ l₂ : filter α) [countable_Inter_filter l₁] [countable_Inter_filter l₂] :
countable_Inter_filter (l₁ ⊔ l₂)

Supremum of two countable_Inter_filters is a countable_Inter_filter.

source
inductive filter.countable_generate_sets {α : Type u_2} (g : set (set α)) :
set α → Prop

filter.countable_generate_sets g is the (sets of the) greatest countable_Inter_filter containing g.

source
def filter.countable_generate {α : Type u_2} (g : set (set α)) :
filter α

filter.countable_generate g is the greatest countable_Inter_filter containing g.

Equations
Instances for filter.countable_generate
source
@[protected, instance]
def filter.countable_generate.countable_Inter_filter {α : Type u_2} (g : set (set α)) :
countable_Inter_filter (filter.countable_generate g)
source
theorem filter.mem_countable_generate_iff {α : Type u_2} {g : set (set α)} {s : set α} :
s ∈ filter.countable_generate g ↔ ∃ (S : set (set α)), S ⊆ g ∧ S.countable ∧ ⋂₀ S ⊆ s

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

source
theorem filter.le_countable_generate_iff_of_countable_Inter_filter {α : Type u_2} {g : set (set α)} {f : filter α} [countable_Inter_filter f] :
f ≤ filter.countable_generate g ↔ g ⊆ f.sets
source
theorem filter.countable_generate_is_greatest {α : Type u_2} (g : set (set α)) :
is_greatest {f : filter α | countable_Inter_filter f ∧ g ⊆ f.sets} (filter.countable_generate g)

countable_generate g is the greatest countable_Inter_filter containing g.