Documentation

Mathlib.Order.Filter.CountableSeparatingOn

Filters with countable intersections and countable separating families #

In this file we prove some facts about a filter with countable intersections property on a type with a countable family of sets that separates points of the space. The main use case is the MeasureTheory.ae filter and a space with countably generated σ-algebra but lemmas apply, e.g., to the residual filter and a T₀ topological space with second countable topology.

To avoid repetition of lemmas for different families of separating sets (measurable sets, open sets, closed sets), all theorems in this file take a predicate p : Set α → Prop as an argument and prove existence of a countable separating family satisfying this predicate by searching for a HasCountableSeparatingOn typeclass instance.

Main definitions #

This typeclass is used in all lemmas in this file to avoid repeating them for open sets, closed sets, and measurable sets.

Main results #

Filters supported on a (sub)singleton #

Let l : Filter α be a filter with countable intersections property. Let p : Set α → Prop be a property such that there exists a countable family of sets satisfying p and separating points of α. Then l is supported on a subsingleton: there exists a subsingleton t such that t ∈ l.

We formalize various versions of this theorem in Filter.exists_subset_subsingleton_mem_of_forall_separating, Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating, Filter.exists_singleton_mem_of_mem_of_forall_separating, Filter.exists_subsingleton_mem_of_forall_separating, and Filter.exists_singleton_mem_of_forall_separating.

Eventually constant functions #

Consider a function f : α → β, a filter l with countable intersections property, and a countable separating family of sets of β. Suppose that for every U from the family, either ∀ᶠ x in l, f x ∈ U or ∀ᶠ x in l, f x ∉ U. Then f is eventually constant along l.

We formalize three versions of this theorem in Filter.exists_mem_eventuallyEq_const_of_eventually_mem_of_forall_separating, Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating, and Filer.exists_eventuallyEq_const_of_forall_separating.

Eventually equal functions #

Two functions are equal along a filter with countable intersections property if the preimages of all sets from a countable separating family of sets are equal along the filter.

We formalize several versions of this theorem in Filter.of_eventually_mem_of_forall_separating_mem_iff, Filter.of_forall_separating_mem_iff, Filter.of_eventually_mem_of_forall_separating_preimage, and Filter.of_forall_separating_preimage.

Keywords #

filter, countable

class HasCountableSeparatingOn (α : Type u_1) (p : Set αProp) (t : Set α) :

We say that a type α has a countable separating family of sets satisfying a predicate p : Set α → Prop on a set t if there exists a countable family of sets S : Set (Set α) such that all sets s ∈ S satisfy p and any two distinct points x y ∈ t, x ≠ y, can be separated by s ∈ S: there exists s ∈ S such that exactly one of x and y belongs to s.

E.g., if α is a T₀ topological space with second countable topology, then it has a countable separating family of open sets and a countable separating family of closed sets.

  • exists_countable_separating : ∃ (S : Set (Set α)), S.Countable (∀ sS, p s) xt, yt, (∀ sS, x s y s)x = y
Instances
    theorem HasCountableSeparatingOn.exists_countable_separating {α : Type u_1} {p : Set αProp} {t : Set α} [self : HasCountableSeparatingOn α p t] :
    ∃ (S : Set (Set α)), S.Countable (∀ sS, p s) xt, yt, (∀ sS, x s y s)x = y
    theorem exists_countable_separating (α : Type u_1) (p : Set αProp) (t : Set α) [h : HasCountableSeparatingOn α p t] :
    ∃ (S : Set (Set α)), S.Countable (∀ sS, p s) xt, yt, (∀ sS, x s y s)x = y
    theorem exists_nonempty_countable_separating (α : Type u_1) {p : Set αProp} {s₀ : Set α} (hp : p s₀) (t : Set α) [HasCountableSeparatingOn α p t] :
    ∃ (S : Set (Set α)), S.Nonempty S.Countable (∀ sS, p s) xt, yt, (∀ sS, x s y s)x = y
    theorem exists_seq_separating (α : Type u_1) {p : Set αProp} {s₀ : Set α} (hp : p s₀) (t : Set α) [HasCountableSeparatingOn α p t] :
    ∃ (S : Set α), (∀ (n : ), p (S n)) xt, yt, (∀ (n : ), x S n y S n)x = y
    theorem HasCountableSeparatingOn.mono {α : Type u_1} {p₁ : Set αProp} {p₂ : Set αProp} {t₁ : Set α} {t₂ : Set α} [h : HasCountableSeparatingOn α p₁ t₁] (hp : ∀ (s : Set α), p₁ sp₂ s) (ht : t₂ t₁) :
    theorem HasCountableSeparatingOn.of_subtype {α : Type u_1} {p : Set αProp} {t : Set α} {q : Set tProp} [h : HasCountableSeparatingOn (↑t) q Set.univ] (hpq : ∀ (U : Set t), q U∃ (V : Set α), p V Subtype.val ⁻¹' V = U) :
    theorem HasCountableSeparatingOn.subtype_iff {α : Type u_1} {p : Set αProp} {t : Set α} :
    HasCountableSeparatingOn (↑t) (fun (u : Set t) => ∃ (v : Set α), p v Subtype.val ⁻¹' v = u) Set.univ HasCountableSeparatingOn α p t

    Filters supported on a (sub)singleton #

    In this section we prove several versions of the following theorem. Let l : Filter α be a filter with countable intersections property. Let p : Set α → Prop be a property such that there exists a countable family of sets satisfying p and separating points of α. Then l is supported on a subsingleton: there exists a subsingleton t such that t ∈ l.

    With extra Nonempty/Set.Nonempty assumptions one can ensure that t is a singleton {x}.

    If s ∈ l, then it suffices to assume that the countable family separates only points of s.

    theorem Filter.exists_subset_subsingleton_mem_of_forall_separating {α : Type u_1} {l : Filter α} [CountableInterFilter l] (p : Set αProp) {s : Set α} [h : HasCountableSeparatingOn α p s] (hs : s l) (hl : ∀ (U : Set α), p UU l U l) :
    ts, t.Subsingleton t l
    theorem Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating {α : Type u_1} {l : Filter α} [CountableInterFilter l] (p : Set αProp) {s : Set α} [HasCountableSeparatingOn α p s] (hs : s l) (hne : s.Nonempty) (hl : ∀ (U : Set α), p UU l U l) :
    as, {a} l
    theorem Filter.exists_singleton_mem_of_mem_of_forall_separating {α : Type u_1} {l : Filter α} [CountableInterFilter l] [Nonempty α] (p : Set αProp) {s : Set α} [HasCountableSeparatingOn α p s] (hs : s l) (hl : ∀ (U : Set α), p UU l U l) :
    ∃ (a : α), {a} l
    theorem Filter.exists_subsingleton_mem_of_forall_separating {α : Type u_1} {l : Filter α} [CountableInterFilter l] (p : Set αProp) [HasCountableSeparatingOn α p Set.univ] (hl : ∀ (U : Set α), p UU l U l) :
    ∃ (s : Set α), s.Subsingleton s l
    theorem Filter.exists_singleton_mem_of_forall_separating {α : Type u_1} {l : Filter α} [CountableInterFilter l] [Nonempty α] (p : Set αProp) [HasCountableSeparatingOn α p Set.univ] (hl : ∀ (U : Set α), p UU l U l) :
    ∃ (x : α), {x} l

    Eventually constant functions #

    In this section we apply theorems from the previous section to the filter Filter.map f l to show that f : α → β is eventually constant along l if for every U from the separating family, either ∀ᶠ x in l, f x ∈ U or ∀ᶠ x in l, f x ∉ U.

    theorem Filter.exists_mem_eventuallyEq_const_of_eventually_mem_of_forall_separating {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : αβ} (p : Set βProp) {s : Set β} [HasCountableSeparatingOn β p s] (hs : ∀ᶠ (x : α) in l, f x s) (hne : s.Nonempty) (h : ∀ (U : Set β), p U(∀ᶠ (x : α) in l, f x U) ∀ᶠ (x : α) in l, f xU) :
    as, f =ᶠ[l] Function.const α a
    theorem Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : αβ} [Nonempty β] (p : Set βProp) {s : Set β} [HasCountableSeparatingOn β p s] (hs : ∀ᶠ (x : α) in l, f x s) (h : ∀ (U : Set β), p U(∀ᶠ (x : α) in l, f x U) ∀ᶠ (x : α) in l, f xU) :
    ∃ (a : β), f =ᶠ[l] Function.const α a
    theorem Filter.exists_eventuallyEq_const_of_forall_separating {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : αβ} [Nonempty β] (p : Set βProp) [HasCountableSeparatingOn β p Set.univ] (h : ∀ (U : Set β), p U(∀ᶠ (x : α) in l, f x U) ∀ᶠ (x : α) in l, f xU) :
    ∃ (a : β), f =ᶠ[l] Function.const α a

    Eventually equal functions #

    In this section we show that two functions are equal along a filter with countable intersections property if the preimages of all sets from a countable separating family of sets are equal along the filter.

    theorem Filter.EventuallyEq.of_eventually_mem_of_forall_separating_mem_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : αβ} {g : αβ} (p : Set βProp) {s : Set β} [h' : HasCountableSeparatingOn β p s] (hf : ∀ᶠ (x : α) in l, f x s) (hg : ∀ᶠ (x : α) in l, g x s) (h : ∀ (U : Set β), p U∀ᶠ (x : α) in l, f x U g x U) :
    f =ᶠ[l] g
    theorem Filter.EventuallyEq.of_forall_separating_mem_iff {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : αβ} {g : αβ} (p : Set βProp) [HasCountableSeparatingOn β p Set.univ] (h : ∀ (U : Set β), p U∀ᶠ (x : α) in l, f x U g x U) :
    f =ᶠ[l] g
    theorem Filter.EventuallyEq.of_eventually_mem_of_forall_separating_preimage {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : αβ} {g : αβ} (p : Set βProp) {s : Set β} [HasCountableSeparatingOn β p s] (hf : ∀ᶠ (x : α) in l, f x s) (hg : ∀ᶠ (x : α) in l, g x s) (h : ∀ (U : Set β), p Uf ⁻¹' U =ᶠ[l] g ⁻¹' U) :
    f =ᶠ[l] g
    theorem Filter.EventuallyEq.of_forall_separating_preimage {α : Type u_1} {β : Type u_2} {l : Filter α} [CountableInterFilter l] {f : αβ} {g : αβ} (p : Set βProp) [HasCountableSeparatingOn β p Set.univ] (h : ∀ (U : Set β), p Uf ⁻¹' U =ᶠ[l] g ⁻¹' U) :
    f =ᶠ[l] g