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

• HasCountableSeparatingOn α p t: a typeclass saying that there exists a countable set family S : Set (Set α) such that all s ∈ S satisfy the predicate p and any two distinct points x y ∈ t, x ≠ y, can be separated by a set s ∈ S. For technical reasons, we formulate the latter property as "for all x y ∈ t, if x ∈ s ↔ y ∈ s for all s ∈ S, then x = y".

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 α) : Prop

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 α)), Set.Countable S ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, 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 α)), Set.Countable S ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, 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 α)), Set.Nonempty S ∧ Set.Countable S ∧ (∀ s ∈ S, p s) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ s ∈ S, 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)) ∧ ∀ x ∈ t, ∀ y ∈ t, (∀ (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₁ s → p₂ s) (ht : t₂ ⊆ t₁) : HasCountableSeparatingOn α p₂ t₂

theorem HasCountableSeparatingOn.of_subtype {α : Type u_1} {p : Set α → Prop} {t : Set α} {q : Set ↑t → Prop} [h : HasCountableSeparatingOn (↑t) q Set.univ] (hpq : ∀ (U : Set ↑t), q U → ∃ (V : Set α), p V ∧ Subtype.val ⁻¹' V = U) : 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 U → U ∈ l ∨ Uᶜ ∈ l) : ∃ t ⊆ s, Set.Subsingleton t ∧ 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 : Set.Nonempty s) (hl : ∀ (U : Set α), p U → U ∈ l ∨ Uᶜ ∈ l) : ∃ a ∈ s, {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 U → U ∈ 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 U → U ∈ l ∨ Uᶜ ∈ l) : ∃ (s : Set α), Set.Subsingleton s ∧ 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 U → U ∈ 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_2} {β : Type u_1} {l : Filter α} [CountableInterFilter l] {f : α → β} (p : Set β → Prop) {s : Set β} [HasCountableSeparatingOn β p s] (hs : ∀ᶠ (x : α) in l, f x ∈ s) (hne : Set.Nonempty s) (h : ∀ (U : Set β), p U → (∀ᶠ (x : α) in l, f x ∈ U) ∨ ∀ᶠ (x : α) in l, f x ∉ U) : ∃ a ∈ s, f =ᶠ[l] Function.const α a

theorem Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating {α : Type u_2} {β : Type u_1} {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 x ∉ U) : ∃ (a : β), f =ᶠ[l] Function.const α a

theorem Filter.exists_eventuallyEq_const_of_forall_separating {α : Type u_2} {β : Type u_1} {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 x ∉ U) : ∃ (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_2} {β : Type u_1} {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_2} {β : Type u_1} {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_2} {β : Type u_1} {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 U → f ⁻¹' U =ᶠ[l] g ⁻¹' U) : f =ᶠ[l] g

theorem Filter.EventuallyEq.of_forall_separating_preimage {α : Type u_2} {β : Type u_1} {l : Filter α} [CountableInterFilter l] {f : α → β} {g : α → β} (p : Set β → Prop) [HasCountableSeparatingOn β p Set.univ] (h : ∀ (U : Set β), p U → f ⁻¹' U =ᶠ[l] g ⁻¹' U) : f =ᶠ[l] g