doc-next-gen

Mathlib.Order.Filter.CountableInter

Module docstring

{"# Filters with countable intersection property

In this file we define CountableInterFilter 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 Mathlib.Topology.GDelta and the MeasureTheory.ae filter defined in Mathlib/MeasureTheory.OuterMeasure/AE.

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, Inf.inf). We also provide a custom constructor Filter.ofCountableInter that deduces two axioms of a Filter from the countable intersection property.

Note that there also exists a typeclass CardinalInterFilter, and thus an alternative spelling of CountableInterFilter as CardinalInterFilter l ℵ₁. The former (defined here) is the preferred spelling; it has the advantage of not requiring the user to import the theory of ordinals.

Tags

filter, countable "}

CountableInterFilter structure
(l : Filter α)
Full source 
/-- A filter `l` has the countable intersection property if for any countable collection
of sets `s ∈ l` their intersection belongs to `l` as well. -/
class CountableInterFilter (l : Filter α) : Prop where
  /-- For a countable collection of sets `s ∈ l`, their intersection belongs to `l` as well. -/
  countable_sInter_mem : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, s ∈ l) → ⋂₀ S⋂₀ S ∈ l
Filter with countable intersection property
Informal description
A filter \( l \) on a type \( \alpha \) is said to have the *countable intersection property* if for any countable collection of sets \( S \subseteq l \), the intersection \( \bigcap S \) also belongs to \( l \).
countable_sInter_mem theorem
{S : Set (Set α)} (hSc : S.Countable) : ⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l
Full source 
theorem countable_sInter_mem {S : Set (Set α)} (hSc : S.Countable) : ⋂₀ S⋂₀ S ∈ l⋂₀ S ∈ l ↔ ∀ s ∈ S, s ∈ l :=
  ⟨fun hS _s hs => mem_of_superset hS (sInter_subset_of_mem hs),
    CountableInterFilter.countable_sInter_mem _ hSc⟩
Countable Intersection Property for Filters: \( \bigcap S \in l \leftrightarrow \forall s \in S, s \in l \)
Informal description
For a filter \( l \) on a type \( \alpha \) with the countable intersection property and a countable collection of sets \( S \subseteq \alpha \), the intersection \( \bigcap S \) belongs to \( l \) if and only if every set in \( S \) belongs to \( l \).
countable_iInter_mem theorem
[Countable ι] {s : ι → Set α} : (⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l
Full source 
theorem countable_iInter_mem [Countable ι] {s : ι → Set α} : (⋂ i, s i) ∈ l(⋂ i, s i) ∈ l ↔ ∀ i, s i ∈ l :=
  sInter_range s ▸ (countable_sInter_mem (countable_range _)).trans forall_mem_range
Countable Intersection Property for Indexed Families: $\bigcap_i s_i \in l \leftrightarrow \forall i, s_i \in l$
Informal description
Let $l$ be a filter on a type $\alpha$ with the countable intersection property, and let $\iota$ be a countable index set. For a family of sets $(s_i)_{i \in \iota}$ in $\alpha$, the intersection $\bigcap_{i \in \iota} s_i$ belongs to $l$ if and only if $s_i \in l$ for every $i \in \iota$.
countable_bInter_mem theorem
{ι : Type*} {S : Set ι} (hS : S.Countable) {s : ∀ i ∈ S, Set α} : (⋂ i, ⋂ hi : i ∈ S, s i ‹_›) ∈ l ↔ ∀ i, ∀ hi : i ∈ S, s i ‹_› ∈ l
Full source 
theorem countable_bInter_mem {ι : Type*} {S : Set ι} (hS : S.Countable) {s : ∀ i ∈ S, Set α} :
    (⋂ i, ⋂ hi : i ∈ S, s i ‹_›) ∈ l(⋂ i, ⋂ hi : i ∈ S, s i ‹_›) ∈ l ↔ ∀ i, ∀ hi : i ∈ S, s i ‹_› ∈ l := by
  rw [biInter_eq_iInter]
  haveI := hS.toEncodable
  exact countable_iInter_mem.trans Subtype.forall
Countable Bounded Intersection Property: $\bigcap_{i \in S} s_i \in l \leftrightarrow \forall i \in S, s_i \in l$
Informal description
Let $l$ be a filter on a type $\alpha$ with the countable intersection property, and let $\iota$ be a type with a countable subset $S \subseteq \iota$. For a family of sets $(s_i)_{i \in S}$ in $\alpha$, the intersection $\bigcap_{i \in S} s_i$ belongs to $l$ if and only if $s_i \in l$ for every $i \in S$.
eventually_countable_forall theorem
[Countable ι] {p : α → ι → Prop} : (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i
Full source 
theorem eventually_countable_forall [Countable ι] {p : α → ι → Prop} :
    (∀ᶠ x in l, ∀ i, p x i) ↔ ∀ i, ∀ᶠ x in l, p x i := by
  simpa only [Filter.Eventually, setOf_forall] using
    @countable_iInter_mem _ _ l _ _ fun i => { x | p x i }
Countable Universal Quantifier Commutation with Filter Eventuality
Informal description
Let $l$ be a filter on a type $\alpha$ with the countable intersection property, and let $\iota$ be a countable index set. For a family of predicates $p_i : \alpha \to \text{Prop}$ indexed by $i \in \iota$, the following equivalence holds: $$ (\forall^l x, \forall i, p_i x) \leftrightarrow \forall i, \forall^l x, p_i x. $$ Here, $\forall^l x, P x$ denotes that the property $P$ holds for $x$ eventually with respect to the filter $l$.
eventually_countable_ball theorem
{ι : Type*} {S : Set ι} (hS : S.Countable) {p : α → ∀ i ∈ S, Prop} : (∀ᶠ x in l, ∀ i hi, p x i hi) ↔ ∀ i hi, ∀ᶠ x in l, p x i hi
Full source 
theorem eventually_countable_ball {ι : Type*} {S : Set ι} (hS : S.Countable)
    {p : α → ∀ i ∈ S, Prop} :
    (∀ᶠ x in l, ∀ i hi, p x i hi) ↔ ∀ i hi, ∀ᶠ x in l, p x i hi := by
  simpa only [Filter.Eventually, setOf_forall] using
    @countable_bInter_mem _ l _ _ _ hS fun i hi => { x | p x i hi }
Countable Universal Quantifier Commutation with Filter Eventuality for Bounded Index Sets
Informal description
Let $l$ be a filter on a type $\alpha$ with the countable intersection property, and let $\iota$ be a type with a countable subset $S \subseteq \iota$. For a family of predicates $p_i : \alpha \to \text{Prop}$ indexed by $i \in S$, the following equivalence holds: $$ (\forall^l x, \forall i \in S, p_i x) \leftrightarrow \forall i \in S, \forall^l x, p_i x. $$ Here, $\forall^l x, P x$ denotes that the property $P$ holds for $x$ eventually with respect to the filter $l$.
EventuallyLE.countable_iUnion theorem
[Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) : ⋃ i, s i ≤ᶠ[l] ⋃ i, t i
Full source 
theorem EventuallyLE.countable_iUnion [Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
    ⋃ i, s i⋃ i, s i ≤ᶠ[l] ⋃ i, t i :=
  (eventually_countable_forall.2 h).mono fun _ hst hs => mem_iUnion.2 <| (mem_iUnion.1 hs).imp hst
Countable Union Preserves Eventual Containment
Informal description
Let $\iota$ be a countable index set, and let $s, t : \iota \to \text{Set } \alpha$ be two families of sets. If for every index $i \in \iota$, the set $s_i$ is eventually contained in $t_i$ with respect to a filter $l$ (i.e., $s_i \leq^l t_i$ for all $i$), then the union $\bigcup_i s_i$ is eventually contained in the union $\bigcup_i t_i$ with respect to the same filter $l$. Here, $A \leq^l B$ means that the set $A$ is eventually contained in $B$ with respect to the filter $l$, i.e., $\{x \mid x \in A \to x \in B\} \in l$.
EventuallyEq.countable_iUnion theorem
[Countable ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) : ⋃ i, s i =ᶠ[l] ⋃ i, t i
Full source 
theorem EventuallyEq.countable_iUnion [Countable ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) :
    ⋃ i, s i⋃ i, s i =ᶠ[l] ⋃ i, t i :=
  (EventuallyLE.countable_iUnion fun i => (h i).le).antisymm
    (EventuallyLE.countable_iUnion fun i => (h i).symm.le)
Countable Union Preserves Eventual Equality
Informal description
Let $\iota$ be a countable index set, and let $s, t : \iota \to \text{Set } \alpha$ be two families of sets. If for every index $i \in \iota$, the sets $s_i$ and $t_i$ are eventually equal with respect to a filter $l$ (i.e., $s_i =^l t_i$ for all $i$), then the unions $\bigcup_i s_i$ and $\bigcup_i t_i$ are also eventually equal with respect to $l$. Here, $A =^l B$ means that the symmetric difference $\{x \mid x \in A \leftrightarrow x \in B\} \in l$.
EventuallyLE.countable_bUnion theorem
{ι : Type*} {S : Set ι} (hS : S.Countable) {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) : ⋃ i ∈ S, s i ‹_› ≤ᶠ[l] ⋃ i ∈ S, t i ‹_›
Full source 
theorem EventuallyLE.countable_bUnion {ι : Type*} {S : Set ι} (hS : S.Countable)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
    ⋃ i ∈ S, s i ‹_›⋃ i ∈ S, s i ‹_› ≤ᶠ[l] ⋃ i ∈ S, t i ‹_› := by
  simp only [biUnion_eq_iUnion]
  haveI := hS.toEncodable
  exact EventuallyLE.countable_iUnion fun i => h i i.2
Eventual Containment Preserved Under Countable Bounded Union
Informal description
Let $\iota$ be a type and $S$ be a countable subset of $\iota$. Given two families of sets $s, t : \forall i \in S, \text{Set } \alpha$ such that for every $i \in S$, the set $s(i)$ is eventually contained in $t(i)$ with respect to a filter $l$ (i.e., $s(i) \leq^l t(i)$ for all $i \in S$), then the bounded union $\bigcup_{i \in S} s(i)$ is eventually contained in the bounded union $\bigcup_{i \in S} t(i)$ with respect to the same filter $l$. Here, $A \leq^l B$ means that the set $\{x \mid x \in A \to x \in B\}$ belongs to the filter $l$.
EventuallyEq.countable_bUnion theorem
{ι : Type*} {S : Set ι} (hS : S.Countable) {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi =ᶠ[l] t i hi) : ⋃ i ∈ S, s i ‹_› =ᶠ[l] ⋃ i ∈ S, t i ‹_›
Full source 
theorem EventuallyEq.countable_bUnion {ι : Type*} {S : Set ι} (hS : S.Countable)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi =ᶠ[l] t i hi) :
    ⋃ i ∈ S, s i ‹_›⋃ i ∈ S, s i ‹_› =ᶠ[l] ⋃ i ∈ S, t i ‹_› :=
  (EventuallyLE.countable_bUnion hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.countable_bUnion hS fun i hi => (h i hi).symm.le)
Countable Bounded Union Preserves Eventual Equality
Informal description
Let $\iota$ be a type and $S$ be a countable subset of $\iota$. Given two families of sets $s, t : \forall i \in S, \text{Set } \alpha$ such that for every $i \in S$, the sets $s(i)$ and $t(i)$ are eventually equal with respect to a filter $l$ (i.e., $s(i) =^l t(i)$ for all $i \in S$), then the bounded unions $\bigcup_{i \in S} s(i)$ and $\bigcup_{i \in S} t(i)$ are also eventually equal with respect to $l$. Here, $A =^l B$ means that the symmetric difference $\{x \mid x \in A \leftrightarrow x \in B\}$ belongs to the filter $l$.
EventuallyLE.countable_iInter theorem
[Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) : ⋂ i, s i ≤ᶠ[l] ⋂ i, t i
Full source 
theorem EventuallyLE.countable_iInter [Countable ι] {s t : ι → Set α} (h : ∀ i, s i ≤ᶠ[l] t i) :
    ⋂ i, s i⋂ i, s i ≤ᶠ[l] ⋂ i, t i :=
  (eventually_countable_forall.2 h).mono fun _ hst hs =>
    mem_iInter.2 fun i => hst _ (mem_iInter.1 hs i)
Countable Intersection Preserves Eventual Containment
Informal description
Let $l$ be a filter on a type $\alpha$ with the countable intersection property, and let $\iota$ be a countable index set. For any two families of sets $s, t : \iota \to \text{Set } \alpha$ such that for every $i \in \iota$, the set $s_i$ is eventually contained in $t_i$ with respect to $l$, then the intersection $\bigcap_i s_i$ is eventually contained in the intersection $\bigcap_i t_i$ with respect to $l$.
EventuallyEq.countable_iInter theorem
[Countable ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) : ⋂ i, s i =ᶠ[l] ⋂ i, t i
Full source 
theorem EventuallyEq.countable_iInter [Countable ι] {s t : ι → Set α} (h : ∀ i, s i =ᶠ[l] t i) :
    ⋂ i, s i⋂ i, s i =ᶠ[l] ⋂ i, t i :=
  (EventuallyLE.countable_iInter fun i => (h i).le).antisymm
    (EventuallyLE.countable_iInter fun i => (h i).symm.le)
Countable Intersection Preserves Eventual Equality
Informal description
Let $\iota$ be a countable index set and let $l$ be a filter on a type $\alpha$ with the countable intersection property. For any two families of sets $s, t : \iota \to \text{Set } \alpha$ such that for every $i \in \iota$, the sets $s_i$ and $t_i$ are eventually equal with respect to $l$, then the intersections $\bigcap_i s_i$ and $\bigcap_i t_i$ are also eventually equal with respect to $l$.
EventuallyLE.countable_bInter theorem
{ι : Type*} {S : Set ι} (hS : S.Countable) {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) : ⋂ i ∈ S, s i ‹_› ≤ᶠ[l] ⋂ i ∈ S, t i ‹_›
Full source 
theorem EventuallyLE.countable_bInter {ι : Type*} {S : Set ι} (hS : S.Countable)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi ≤ᶠ[l] t i hi) :
    ⋂ i ∈ S, s i ‹_›⋂ i ∈ S, s i ‹_› ≤ᶠ[l] ⋂ i ∈ S, t i ‹_› := by
  simp only [biInter_eq_iInter]
  haveI := hS.toEncodable
  exact EventuallyLE.countable_iInter fun i => h i i.2
Eventual Containment Preserved under Countable Bounded Intersection
Informal description
Let $\iota$ be a type, $S$ be a countable subset of $\iota$, and $l$ be a filter on a type $\alpha$ with the countable intersection property. For any two families of sets $s, t : \forall i \in S, \text{Set } \alpha$ such that for every $i \in S$ and $h_i : i \in S$, the set $s(i, h_i)$ is eventually contained in $t(i, h_i)$ with respect to $l$, then the bounded intersection $\bigcap_{i \in S} s(i, h_i)$ is eventually contained in the bounded intersection $\bigcap_{i \in S} t(i, h_i)$ with respect to $l$.
EventuallyEq.countable_bInter theorem
{ι : Type*} {S : Set ι} (hS : S.Countable) {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi =ᶠ[l] t i hi) : ⋂ i ∈ S, s i ‹_› =ᶠ[l] ⋂ i ∈ S, t i ‹_›
Full source 
theorem EventuallyEq.countable_bInter {ι : Type*} {S : Set ι} (hS : S.Countable)
    {s t : ∀ i ∈ S, Set α} (h : ∀ i hi, s i hi =ᶠ[l] t i hi) :
    ⋂ i ∈ S, s i ‹_›⋂ i ∈ S, s i ‹_› =ᶠ[l] ⋂ i ∈ S, t i ‹_› :=
  (EventuallyLE.countable_bInter hS fun i hi => (h i hi).le).antisymm
    (EventuallyLE.countable_bInter hS fun i hi => (h i hi).symm.le)
Eventual Equality Preserved under Countable Bounded Intersection
Informal description
Let $\iota$ be a type, $S$ be a countable subset of $\iota$, and $l$ be a filter on a type $\alpha$ with the countable intersection property. For any two families of sets $s, t : \forall i \in S, \text{Set } \alpha$ such that for every $i \in S$ and $h_i : i \in S$, the sets $s(i, h_i)$ and $t(i, h_i)$ are eventually equal with respect to $l$, then the bounded intersections $\bigcap_{i \in S} s(i, h_i)$ and $\bigcap_{i \in S} t(i, h_i)$ are also eventually equal with respect to $l$.
Filter.ofCountableInter definition
(l : Set (Set α)) (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α
Full source 
/-- Construct a filter with countable intersection property. This constructor deduces
`Filter.univ_sets` and `Filter.inter_sets` from the countable intersection property. -/
def Filter.ofCountableInter (l : Set (Set α))
    (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : Filter α where
  sets := l
  univ_sets := @sInter_empty α ▸ hl _ countable_empty (empty_subset _)
  sets_of_superset := h_mono _ _
  inter_sets {s t} hs ht := sInter_pair s t ▸
    hl _ ((countable_singleton _).insert _) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
Filter construction from countable intersection property
Informal description
Given a collection \( l \) of subsets of a type \( \alpha \) that is closed under countable intersections (i.e., for any countable subset \( S \subseteq l \), the intersection \( \bigcap S \) belongs to \( l \)) and is upward-closed (i.e., if \( s \in l \) and \( s \subseteq t \), then \( t \in l \)), the function constructs a filter with \( l \) as its filter sets. The filter axioms (containing the full set, being closed under supersets, and closed under finite intersections) are derived from the given properties of \( l \).
Filter.countableInter_ofCountableInter instance
(l : Set (Set α)) (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) : CountableInterFilter (Filter.ofCountableInter l hl h_mono)
Full source 
instance Filter.countableInter_ofCountableInter (l : Set (Set α))
    (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S⋂₀ S ∈ l)
    (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) :
    CountableInterFilter (Filter.ofCountableInter l hl h_mono) :=
  ⟨hl⟩
Countable Intersection Property of Constructed Filter
Informal description
Given a collection \( l \) of subsets of a type \( \alpha \) that is closed under countable intersections (i.e., for any countable subset \( S \subseteq l \), the intersection \( \bigcap S \) belongs to \( l \)) and is upward-closed (i.e., if \( s \in l \) and \( s \subseteq t \), then \( t \in l \)), the filter constructed from \( l \) using `Filter.ofCountableInter` has the countable intersection property.
Filter.mem_ofCountableInter theorem
{l : Set (Set α)} (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l) {s : Set α} : s ∈ Filter.ofCountableInter l hl h_mono ↔ s ∈ l
Full source 
@[simp]
theorem Filter.mem_ofCountableInter {l : Set (Set α)}
    (hl : ∀ S : Set (Set α), S.Countable → S ⊆ l → ⋂₀ S⋂₀ S ∈ l) (h_mono : ∀ s t, s ∈ l → s ⊆ t → t ∈ l)
    {s : Set α} : s ∈ Filter.ofCountableInter l hl h_monos ∈ Filter.ofCountableInter l hl h_mono ↔ s ∈ l :=
  Iff.rfl
Membership in Filter Constructed from Countable Intersection Property
Informal description
For a collection $l$ of subsets of a type $\alpha$ that is closed under countable intersections (i.e., for any countable $S \subseteq l$, the intersection $\bigcap S$ belongs to $l$) and is upward-closed (i.e., if $s \in l$ and $s \subseteq t$, then $t \in l$), a subset $s$ of $\alpha$ belongs to the filter constructed from $l$ if and only if $s$ belongs to $l$.
Filter.ofCountableUnion definition
(l : Set (Set α)) (hUnion : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S ∈ l) (hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α
Full source 
/-- Construct a filter with countable intersection property.
Similarly to `Filter.comk`, a set belongs to this filter if its complement satisfies the property.
Similarly to `Filter.ofCountableInter`,
this constructor deduces some properties from the countable intersection property
which becomes the countable union property because we take complements of all sets. -/
def Filter.ofCountableUnion (l : Set (Set α))
    (hUnion : ∀ S : Set (Set α), S.Countable → (∀ s ∈ S, s ∈ l) → ⋃₀ S⋃₀ S ∈ l)
    (hmono : ∀ t ∈ l, ∀ s ⊆ t, s ∈ l) : Filter α := by
  refine .ofCountableInter {s | sᶜ ∈ l} (fun S hSc hSp ↦ ?_) fun s t ht hsub ↦ ?_
  · rw [mem_setOf_eq, compl_sInter]
    apply hUnion (complcompl '' S) (hSc.image _)
    intro s hs
    rw [mem_image] at hs
    rcases hs with ⟨t, ht, rfl⟩
    apply hSp ht
  · rw [mem_setOf_eq]
    rw [← compl_subset_compl] at hsub
    exact hmono sᶜ ht tᶜ hsub
Filter construction from countable union property
Informal description
Given a collection \( l \) of subsets of a type \( \alpha \) that is closed under countable unions (i.e., for any countable subset \( S \subseteq l \), the union \( \bigcup S \) belongs to \( l \)) and is downward-closed (i.e., if \( t \in l \) and \( s \subseteq t \), then \( s \in l \)), the function constructs a filter where a set \( s \) belongs to the filter if and only if its complement \( s^c \) belongs to \( l \). The filter axioms are derived from these properties of \( l \).
Filter.countableInter_ofCountableUnion instance
(l : Set (Set α)) (h₁ h₂) : CountableInterFilter (Filter.ofCountableUnion l h₁ h₂)
Full source 
instance Filter.countableInter_ofCountableUnion (l : Set (Set α)) (h₁ h₂) :
    CountableInterFilter (Filter.ofCountableUnion l h₁ h₂) :=
  countableInter_ofCountableInter ..
Countable Intersection Property of Filter Constructed from Countable Union Property
Informal description
Given a collection \( l \) of subsets of a type \( \alpha \) that is closed under countable unions (i.e., for any countable subset \( S \subseteq l \), the union \( \bigcup S \) belongs to \( l \)) and is downward-closed (i.e., if \( t \in l \) and \( s \subseteq t \), then \( s \in l \)), the filter constructed from \( l \) using `Filter.ofCountableUnion` has the countable intersection property.
Filter.mem_ofCountableUnion theorem
{l : Set (Set α)} {hunion hmono s} : s ∈ ofCountableUnion l hunion hmono ↔ l sᶜ
Full source 
@[simp]
theorem Filter.mem_ofCountableUnion {l : Set (Set α)} {hunion hmono s} :
    s ∈ ofCountableUnion l hunion hmonos ∈ ofCountableUnion l hunion hmono ↔ l sᶜ :=
  Iff.rfl
Membership Criterion for Filter Constructed from Countable Union Property
Informal description
For a collection $l$ of subsets of a type $\alpha$ that is closed under countable unions and downward-closed, a set $s$ belongs to the filter constructed from $l$ if and only if its complement $s^c$ belongs to $l$. In other words, $s \in \text{ofCountableUnion}\,l\,h_{\text{union}}\,h_{\text{mono}} \leftrightarrow s^c \in l$.
countableInterFilter_principal instance
(s : Set α) : CountableInterFilter (𝓟 s)
Full source 
instance countableInterFilter_principal (s : Set α) : CountableInterFilter (𝓟 s) :=
  ⟨fun _ _ hS => subset_sInter hS⟩
Principal Filters Have Countable Intersection Property
Informal description
For any set $s$ in a type $\alpha$, the principal filter $\mathfrak{p}(s)$ has the countable intersection property. That is, for any countable collection of subsets of $s$, their intersection is also in the principal filter.
instCountableInterFilterComap instance
(l : Filter β) [CountableInterFilter l] (f : α → β) : CountableInterFilter (comap f l)
Full source 
instance (l : Filter β) [CountableInterFilter l] (f : α → β) :
    CountableInterFilter (comap f l) := by
  refine ⟨fun S hSc hS => ?_⟩
  choose! t htl ht using hS
  have : (⋂ s ∈ S, t s) ∈ l := (countable_bInter_mem hSc).2 htl
  refine ⟨_, this, ?_⟩
  simpa [preimage_iInter] using iInter₂_mono ht
Countable Intersection Property is Preserved under Preimage Filters
Informal description
For any filter $l$ on a type $\beta$ with the countable intersection property and any function $f : \alpha \to \beta$, the preimage filter $\text{comap } f \ l$ on $\alpha$ also has the countable intersection property.
instCountableInterFilterMap instance
(l : Filter α) [CountableInterFilter l] (f : α → β) : CountableInterFilter (map f l)
Full source 
instance (l : Filter α) [CountableInterFilter l] (f : α → β) : CountableInterFilter (map f l) := by
  refine ⟨fun S hSc hS => ?_⟩
  simp only [mem_map, sInter_eq_biInter, preimage_iInter₂] at hS ⊢
  exact (countable_bInter_mem hSc).2 hS
Countable Intersection Property is Preserved Under Filter Mapping
Informal description
For any filter $l$ on a type $\alpha$ with the countable intersection property and any function $f : \alpha \to \beta$, the image filter $\text{map } f \ l$ on $\beta$ also has the countable intersection property. This means that if $l$ is closed under countable intersections, then the filter generated by the images of sets in $l$ under $f$ is also closed under countable intersections.
countableInterFilter_inf instance
(l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] : CountableInterFilter (l₁ ⊓ l₂)
Full source 
/-- Infimum of two `CountableInterFilter`s is a `CountableInterFilter`. This is useful, e.g.,
to automatically get an instance for `residual α ⊓ 𝓟 s`. -/
instance countableInterFilter_inf (l₁ l₂ : Filter α) [CountableInterFilter l₁]
    [CountableInterFilter l₂] : CountableInterFilter (l₁ ⊓ l₂) := by
  refine ⟨fun S hSc hS => ?_⟩
  choose s hs t ht hst using hS
  replace hs : (⋂ i ∈ S, s i ‹_›) ∈ l₁ := (countable_bInter_mem hSc).2 hs
  replace ht : (⋂ i ∈ S, t i ‹_›) ∈ l₂ := (countable_bInter_mem hSc).2 ht
  refine mem_of_superset (inter_mem_inf hs ht) (subset_sInter fun i hi => ?_)
  rw [hst i hi]
  apply inter_subset_inter <;> exact iInter_subset_of_subset i (iInter_subset _ _)
Infimum of Countable Intersection Filters is a Countable Intersection Filter
Informal description
For any two filters \( l_1 \) and \( l_2 \) on a type \( \alpha \) with the countable intersection property, their infimum \( l_1 \sqcap l_2 \) also has the countable intersection property. This means that if both \( l_1 \) and \( l_2 \) are closed under countable intersections, then their infimum filter is also closed under countable intersections.
countableInterFilter_sup instance
(l₁ l₂ : Filter α) [CountableInterFilter l₁] [CountableInterFilter l₂] : CountableInterFilter (l₁ ⊔ l₂)
Full source 
/-- Supremum of two `CountableInterFilter`s is a `CountableInterFilter`. -/
instance countableInterFilter_sup (l₁ l₂ : Filter α) [CountableInterFilter l₁]
    [CountableInterFilter l₂] : CountableInterFilter (l₁ ⊔ l₂) := by
  refine ⟨fun S hSc hS => ⟨?_, ?_⟩⟩ <;> refine (countable_sInter_mem hSc).2 fun s hs => ?_
  exacts [(hS s hs).1, (hS s hs).2]
Supremum of Countable Intersection Filters is a Countable Intersection Filter
Informal description
For any two filters \( l_1 \) and \( l_2 \) on a type \( \alpha \) with the countable intersection property, their supremum \( l_1 \sqcup l_2 \) also has the countable intersection property. This means that if both \( l_1 \) and \( l_2 \) are closed under countable intersections, then their supremum filter is also closed under countable intersections.
CountableInterFilter.curry instance
{α β : Type*} {l : Filter α} {m : Filter β} [CountableInterFilter l] [CountableInterFilter m] : CountableInterFilter (l.curry m)
Full source 
instance CountableInterFilter.curry {α β : Type*} {l : Filter α} {m : Filter β}
    [CountableInterFilter l] [CountableInterFilter m] : CountableInterFilter (l.curry m) := ⟨by
  intro S Sct hS
  simp_rw [mem_curry_iff, mem_sInter, eventually_countable_ball (p := fun _ _ _ => (_ ,_) ∈ _) Sct,
    eventually_countable_ball (p := fun _ _ _ => ∀ᶠ (_ : β) in m, _)  Sct, ← mem_curry_iff]
  exact hS⟩
Countable Intersection Property Preserved by Filter Currying
Informal description
For any two types $\alpha$ and $\beta$, if $l$ is a filter on $\alpha$ with the countable intersection property and $m$ is a filter on $\beta$ with the countable intersection property, then the curried filter $l.\text{curry}\, m$ on $\alpha \times \beta$ also has the countable intersection property.
Filter.CountableGenerateSets inductive
: Set α → Prop
Full source 
/-- `Filter.CountableGenerateSets g` is the (sets of the)
greatest `countableInterFilter` containing `g`. -/
inductive CountableGenerateSets : Set α → Prop
  | basic {s : Set α} : s ∈ g → CountableGenerateSets s
  | univ : CountableGenerateSets univ
  | superset {s t : Set α} : CountableGenerateSets s → s ⊆ t → CountableGenerateSets t
  | sInter {S : Set (Set α)} :
    S.Countable → (∀ s ∈ S, CountableGenerateSets s) → CountableGenerateSets (⋂₀ S)
Countable generation of filter sets
Informal description
The predicate `Filter.CountableGenerateSets g` defines the collection of sets that belong to the greatest countable intersection filter containing the set `g`. A countable intersection filter is one where any countable intersection of sets in the filter is also in the filter.
Filter.countableGenerate definition
: Filter α
Full source 
/-- `Filter.countableGenerate g` is the greatest `countableInterFilter` containing `g`. -/
def countableGenerate : Filter α :=
  ofCountableInter (CountableGenerateSets g) (fun _ => CountableGenerateSets.sInter) fun _ _ =>
    CountableGenerateSets.superset
Greatest countable intersection filter containing a set
Informal description
The filter `Filter.countableGenerate g` is the greatest filter containing the set `g` that satisfies the countable intersection property, meaning that any countable intersection of sets in the filter is also in the filter. More precisely, a set `s` is in `Filter.countableGenerate g` if and only if there exists a countable subset `S` of `g` such that the intersection of all sets in `S` is contained in `s`.
Filter.instCountableInterFilterCountableGenerate instance
: CountableInterFilter (countableGenerate g)
Full source 
instance : CountableInterFilter (countableGenerate g) := by
  delta countableGenerate; infer_instance
Countable Intersection Property of the Generated Filter
Informal description
The filter `countableGenerate g` on a type $\alpha$ has the countable intersection property, meaning that for any countable collection of sets in the filter, their intersection is also in the filter.
Filter.mem_countableGenerate_iff theorem
{s : Set α} : s ∈ countableGenerate g ↔ ∃ S : Set (Set α), S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s
Full source 
/-- A set is in the `countableInterFilter` generated by `g` if and only if
it contains a countable intersection of elements of `g`. -/
theorem mem_countableGenerate_iff {s : Set α} :
    s ∈ countableGenerate gs ∈ countableGenerate g ↔ ∃ S : Set (Set α), S ⊆ g ∧ S.Countable ∧ ⋂₀ S ⊆ s := by
  constructor <;> intro h
  · induction h with
    | @basic s hs => exact ⟨{s}, by simp [hs, subset_refl]⟩
    | univ => exact ⟨∅, by simp⟩
    | superset _ _ ih => refine Exists.imp (fun S => ?_) ih; tauto
    | @sInter S Sct _ ih =>
      choose T Tg Tct hT using ih
      refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa, Sct.biUnion Tct, ?_⟩
      apply subset_sInter
      intro s H
      exact subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)
  rcases h with ⟨S, Sg, Sct, hS⟩
  refine mem_of_superset ((countable_sInter_mem Sct).mpr ?_) hS
  intro s H
  exact CountableGenerateSets.basic (Sg H)
Characterization of Membership in Countable Generate Filter: $s \in \text{countableGenerate}\ g \leftrightarrow \exists S \subseteq g, \text{countable}\ S \land \bigcap S \subseteq s$
Informal description
A set $s$ belongs to the filter $\text{countableGenerate}\ g$ if and only if there exists a countable subset $S \subseteq g$ such that the intersection $\bigcap S$ is contained in $s$.
Filter.le_countableGenerate_iff_of_countableInterFilter theorem
{f : Filter α} [CountableInterFilter f] : f ≤ countableGenerate g ↔ g ⊆ f.sets
Full source 
theorem le_countableGenerate_iff_of_countableInterFilter {f : Filter α} [CountableInterFilter f] :
    f ≤ countableGenerate g ↔ g ⊆ f.sets := by
  constructor <;> intro h
  · exact subset_trans (fun s => CountableGenerateSets.basic) h
  intro s hs
  induction hs with
  | basic hs => exact h hs
  | univ => exact univ_mem
  | superset _ st ih => exact mem_of_superset ih st
  | sInter Sct _ ih => exact (countable_sInter_mem Sct).mpr ih
Characterization of Filter Containment in Countable Generate Filter: $f \leq \text{countableGenerate}\ g \leftrightarrow g \subseteq f$
Informal description
For a filter $f$ on a type $\alpha$ with the countable intersection property and a set $g$ of subsets of $\alpha$, the filter $f$ is contained in the countable generate filter of $g$ if and only if every set in $g$ belongs to $f$.
Filter.countableGenerate_isGreatest theorem
: IsGreatest {f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets} (countableGenerate g)
Full source 
/-- `countableGenerate g` is the greatest `countableInterFilter` containing `g`. -/
theorem countableGenerate_isGreatest :
    IsGreatest { f : Filter α | CountableInterFilter f ∧ g ⊆ f.sets } (countableGenerate g) := by
  refine ⟨⟨inferInstance, fun s => CountableGenerateSets.basic⟩, ?_⟩
  rintro f ⟨fct, hf⟩
  rwa [@le_countableGenerate_iff_of_countableInterFilter _ _ _ fct]
Greatest Countable Intersection Filter Containing a Set
Informal description
The filter `countableGenerate g` is the greatest filter containing the set `g` that satisfies the countable intersection property. That is, for any filter `f` on a type `α` with the countable intersection property such that `g ⊆ f.sets`, we have `f ≤ countableGenerate g`.