# 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 #

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

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 : ] :
∃ (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 : ] :
∃ (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 α) [] :
∃ (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 α) [] :
∃ (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 : ] (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

### 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) :
ts, t.Subsingleton 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 : 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 : } [] (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 : Set α), s.Subsingleton 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_1} {β : Type u_2} {l : } {f : αβ} (p : Set βProp) {s : Set β} [] (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]
theorem Filter.exists_eventuallyEq_const_of_eventually_mem_of_forall_separating {α : Type u_1} {β : Type u_2} {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 xU) :
∃ (a : β), f =ᶠ[l]
theorem Filter.exists_eventuallyEq_const_of_forall_separating {α : Type u_1} {β : Type u_2} {l : } {f : αβ} [] (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]

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