# 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.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 α) :
• exists_countable_separating : S, (∀ (s : Set α), s Sp s) ∀ (x : α), x t∀ (y : α), y t(∀ (s : Set α), s S → (x s y s)) → x = y

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.

Instances
theorem exists_countable_separating (α : Type u_1) (p : Set αProp) (t : Set α) [h : ] :
S, ((s : Set α) → s Sp s) ∀ (x : α), x t∀ (y : α), y t(∀ (s : Set α), 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 α) [] :
S, ((s : Set α) → s Sp s) ∀ (x : α), x t∀ (y : α), y t(∀ (s : Set α), 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 α) [] :
S, ((n : ) → p (S n)) ∀ (x : α), x t∀ (y : α), 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 : ] (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 UV, p V Subtype.val ⁻¹' V = U) :

### 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 : } (p : Set αProp) {s : Set α} [h : ] (hs : s l) (hl : ∀ (U : Set α), p UU l U l) :
t, t s t l
theorem Filter.exists_mem_singleton_mem_of_mem_of_nonempty_of_forall_separating {α : Type u_1} {l : } (p : Set αProp) {s : Set α} [] (hs : s l) (hne : ) (hl : ∀ (U : Set α), p UU l U l) :
a, a s {a} l
theorem Filter.exists_singleton_mem_of_mem_of_forall_separating {α : Type u_1} {l : } [] (p : Set αProp) {s : Set α} [] (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 : } (p : Set αProp) [HasCountableSeparatingOn α p Set.univ] (hl : ∀ (U : Set α), p UU l U l) :
s, s l
theorem Filter.exists_singleton_mem_of_forall_separating {α : Type u_1} {l : } [] (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_2} {β : Type u_1} {l : } {f : αβ} (p : Set βProp) {s : Set β} [] (hs : ∀ᶠ (x : α) in l, f x s) (hne : ) (h : ∀ (U : Set β), p U(∀ᶠ (x : α) in l, f x U) ∀ᶠ (x : α) in l, ¬f x U) :
a, a s f =ᶠ[l]
theorem Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating {α : Type u_2} {β : Type u_1} {l : } {f : αβ} [] (p : Set βProp) {s : Set β} [] (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]
theorem Filter.exists_eventuallyEq_const_of_forall_separating {α : Type u_2} {β : Type u_1} {l : } {f : αβ} [] (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]

### 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 : } {f : αβ} {g : αβ} (p : Set βProp) {s : Set β} [h' : ] (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 : } {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 : } {f : αβ} {g : αβ} (p : Set βProp) {s : Set β} [] (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_2} {β : Type u_1} {l : } {f : αβ} {g : αβ} (p : Set βProp) [HasCountableSeparatingOn β p Set.univ] (h : ∀ (U : Set β), p Uf ⁻¹' U =ᶠ[l] g ⁻¹' U) :
f =ᶠ[l] g