Mathlib.Order.Filter.CountablyGenerated

Filter.IsCountablyGenerated structure

(f : Filter α)

Full source

/-- `IsCountablyGenerated f` means `f = generate s` for some countable `s`. -/
class IsCountablyGenerated (f : Filter α) : Prop where
  /-- There exists a countable set that generates the filter. -/
  out : ∃ s : Set (Set α), s.Countable ∧ f = generate s

Countably generated filter

Informal description

A filter `f` on a type `α` is countably generated if there exists a countable family of sets that generates `f`. This means that `f` can be expressed as the filter generated by some countable collection of subsets of `α`.

Filter.IsCountableBasis structure

(p : ι → Prop) (s : ι → Set α) : Prop extends IsBasis p s

Full source

/-- `IsCountableBasis p s` means the image of `s` bounded by `p` is a countable filter basis. -/
structure IsCountableBasis (p : ι → Prop) (s : ι → Set α) : Prop extends IsBasis p s where
  /-- The set of `i` that satisfy the predicate `p` is countable. -/
  countable : (setOf p).Countable

Countable filter basis

Informal description

A family of sets `s : ι → Set α` indexed by a predicate `p : ι → Prop` is called a *countable basis* if the image of `s` restricted by `p` forms a countable filter basis. This means that the collection `{s i | p i}` is countable and satisfies the conditions of a filter basis (nonempty and closed under finite intersections).

Filter.HasCountableBasis structure

(l : Filter α) (p : ι → Prop) (s : ι → Set α) : Prop
    extends HasBasis l p s

Full source

/-- We say that a filter `l` has a countable basis `s : ι → Set α` bounded by `p : ι → Prop`,
if `t ∈ l` if and only if `t` includes `s i` for some `i` such that `p i`, and the set
defined by `p` is countable. -/
structure HasCountableBasis (l : Filter α) (p : ι → Prop) (s : ι → Set α) : Prop
    extends HasBasis l p s where
  /-- The set of `i` that satisfy the predicate `p` is countable. -/
  countable : (setOf p).Countable

Filter with countable basis

Informal description

A filter $l$ on a type $\alpha$ is said to have a countable basis consisting of sets $s_i$ indexed by $i \in \iota$ and bounded by a predicate $p : \iota \to \text{Prop}$ if: 1. A set $t$ belongs to $l$ if and only if there exists an index $i$ such that $p(i)$ holds and $s_i \subseteq t$. 2. The set of indices $\{i \mid p(i)\}$ is countable. This structure extends the notion of a filter having a basis by adding the countability condition on the index set.

Filter.CountableFilterBasis structure

(α : Type*) extends FilterBasis α

Full source

/-- A countable filter basis `B` on a type `α` is a nonempty countable collection of sets of `α`
such that the intersection of two elements of this collection contains some element
of the collection. -/
structure CountableFilterBasis (α : Type*) extends FilterBasis α where
  /-- The set of sets of the filter basis is countable. -/
  countable : sets.Countable

Countable Filter Basis

Informal description

A countable filter basis on a type $\alpha$ is a nonempty countable collection of subsets of $\alpha$ such that the intersection of any two sets in the collection contains another set from the collection. This structure extends the general notion of a filter basis by adding the countability condition.

Filter.Nat.inhabitedCountableFilterBasis instance

: Inhabited (CountableFilterBasis ℕ)

Full source

instance Nat.inhabitedCountableFilterBasis : Inhabited (CountableFilterBasis ℕ) :=
  ⟨⟨default, countable_range fun n => Ici n⟩⟩

Countable Filter Basis Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ have a canonical countable filter basis structure.

Filter.HasCountableBasis.isCountablyGenerated theorem

{f : Filter α} {p : ι → Prop} {s : ι → Set α} (h : f.HasCountableBasis p s) : f.IsCountablyGenerated

Full source

theorem HasCountableBasis.isCountablyGenerated {f : Filter α} {p : ι → Prop} {s : ι → Set α}
    (h : f.HasCountableBasis p s) : f.IsCountablyGenerated :=
  ⟨⟨{ t | ∃ i, p i ∧ s i = t }, h.countable.image s, h.toHasBasis.eq_generate⟩⟩

Filters with countable basis are countably generated

Informal description

Let $f$ be a filter on a type $\alpha$ with a countable basis consisting of sets $s_i$ indexed by $i \in \iota$ and bounded by a predicate $p : \iota \to \text{Prop}$. Then $f$ is countably generated.

Filter.HasBasis.isCountablyGenerated theorem

[Countable ι] {f : Filter α} {p : ι → Prop} {s : ι → Set α} (h : f.HasBasis p s) : f.IsCountablyGenerated

Full source

theorem HasBasis.isCountablyGenerated [Countable ι] {f : Filter α} {p : ι → Prop} {s : ι → Set α}
    (h : f.HasBasis p s) : f.IsCountablyGenerated :=
  HasCountableBasis.isCountablyGenerated ⟨h, to_countable _⟩

Filters with countable index basis are countably generated

Informal description

Let $\alpha$ be a type, $\iota$ a countable type, $f$ a filter on $\alpha$, $p : \iota \to \text{Prop}$ a predicate, and $s : \iota \to \text{Set } \alpha$ a family of sets. If $f$ has a basis consisting of the sets $\{s_i \mid p_i\}$, then $f$ is countably generated.

Filter.antitone_seq_of_seq theorem

(s : ℕ → Set α) : ∃ t : ℕ → Set α, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i)

Full source

theorem antitone_seq_of_seq (s : ℕ → Set α) :
    ∃ t : ℕ → Set α, Antitone t ∧ ⨅ i, 𝓟 (s i) = ⨅ i, 𝓟 (t i) := by
  use fun n => ⋂ m ≤ n, s m; constructor
  · exact fun i j hij => biInter_mono (Iic_subset_Iic.2 hij) fun n _ => Subset.rfl
  apply le_antisymm <;> rw [le_iInf_iff] <;> intro i
  · rw [le_principal_iff]
    refine (biInter_mem (finite_le_nat _)).2 fun j _ => ?_
    exact mem_iInf_of_mem j (mem_principal_self _)
  · refine iInf_le_of_le i (principal_mono.2 <| iInter₂_subset i ?_)
    rfl

Existence of Antitone Sequence with Same Filter Infimum

Informal description

For any sequence of sets $(s_n)_{n \in \mathbb{N}}$ in a type $\alpha$, there exists an antitone sequence of sets $(t_n)_{n \in \mathbb{N}}$ (i.e., $t_{n+1} \subseteq t_n$ for all $n$) such that the infimum of the principal filters generated by the $s_n$ equals the infimum of the principal filters generated by the $t_n$. In other words, $$\bigsqcap_{n \in \mathbb{N}} \mathfrak{P}(s_n) = \bigsqcap_{n \in \mathbb{N}} \mathfrak{P}(t_n).$$

Filter.countable_biInf_eq_iInf_seq theorem

 [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (Bne : B.Nonempty) (f : ι → α) :
  ∃ x : ℕ → ι, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Full source

theorem countable_biInf_eq_iInf_seq [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable)
    (Bne : B.Nonempty) (f : ι → α) : ∃ x : ℕ → ι, ⨅ t ∈ B, f t = ⨅ i, f (x i) :=
  let ⟨g, hg⟩ := Bcbl.exists_eq_range Bne
  ⟨g, hg.symm ▸ iInf_range⟩

Countable Infimum as Sequential Infimum in Complete Lattices

Informal description

Let $\alpha$ be a complete lattice, $B$ a nonempty countable subset of $\iota$, and $f : \iota \to \alpha$ a function. Then there exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $\iota$ such that the infimum of $f$ over $B$ equals the infimum of $f$ over the sequence, i.e., $$\bigsqcap_{t \in B} f(t) = \bigsqcap_{i \in \mathbb{N}} f(x_i).$$

Filter.countable_biInf_eq_iInf_seq' theorem

 [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (f : ι → α) {i₀ : ι} (h : f i₀ = ⊤) :
  ∃ x : ℕ → ι, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Full source

theorem countable_biInf_eq_iInf_seq' [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable)
    (f : ι → α) {i₀ : ι} (h : f i₀ = ⊤) : ∃ x : ℕ → ι, ⨅ t ∈ B, f t = ⨅ i, f (x i) := by
  rcases B.eq_empty_or_nonempty with hB | Bnonempty
  · rw [hB, iInf_emptyset]
    use fun _ => i₀
    simp [h]
  · exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f

Countable Infimum as Sequential Infimum in Complete Lattices (Top Case)

Informal description

Let $\alpha$ be a complete lattice, $B$ a countable subset of $\iota$, and $f : \iota \to \alpha$ a function such that $f(i_0) = \top$ for some $i_0 \in \iota$. Then there exists a sequence $(x_n)_{n \in \mathbb{N}}$ in $\iota$ such that the infimum of $f$ over $B$ equals the infimum of $f$ over the sequence, i.e., $$\bigsqcap_{t \in B} f(t) = \bigsqcap_{i \in \mathbb{N}} f(x_i).$$

Filter.countable_biInf_principal_eq_seq_iInf theorem

{B : Set (Set α)} (Bcbl : B.Countable) : ∃ x : ℕ → Set α, ⨅ t ∈ B, 𝓟 t = ⨅ i, 𝓟 (x i)

Full source

theorem countable_biInf_principal_eq_seq_iInf {B : Set (Set α)} (Bcbl : B.Countable) :
    ∃ x : ℕ → Set α, ⨅ t ∈ B, 𝓟 t = ⨅ i, 𝓟 (x i) :=
  countable_biInf_eq_iInf_seq' Bcbl 𝓟 principal_univ

Countable Infimum of Principal Filters as Sequential Infimum

Informal description

For any countable collection of sets $B$ in a type $\alpha$, there exists a sequence of sets $(x_n)_{n \in \mathbb{N}}$ such that the infimum of the principal filters generated by the sets in $B$ is equal to the infimum of the principal filters generated by the sets in the sequence, i.e., $$\bigsqcap_{t \in B} \mathfrak{P}(t) = \bigsqcap_{i \in \mathbb{N}} \mathfrak{P}(x_i),$$ where $\mathfrak{P}(s)$ denotes the principal filter generated by a set $s$.

Filter.HasAntitoneBasis.mem_iff theorem

 [Preorder ι] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) {t : Set α} : t ∈ l ↔ ∃ i, s i ⊆ t

Full source

protected theorem HasAntitoneBasis.mem_iff [Preorder ι] {l : Filter α} {s : ι → Set α}
    (hs : l.HasAntitoneBasis s) {t : Set α} : t ∈ lt ∈ l ↔ ∃ i, s i ⊆ t :=
  hs.toHasBasis.mem_iff.trans <| by simp only [exists_prop, true_and]

Membership Criterion for Filters with Antitone Basis

Informal description

Let $\alpha$ be a type, $\iota$ be a preorder, $l$ be a filter on $\alpha$, and $s : \iota \to \text{Set} \alpha$ be an antitone basis for $l$. Then, for any subset $t \subseteq \alpha$, we have $t \in l$ if and only if there exists an index $i \in \iota$ such that $s(i) \subseteq t$.

Filter.HasAntitoneBasis.mem theorem

[Preorder ι] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) (i : ι) : s i ∈ l

Full source

protected theorem HasAntitoneBasis.mem [Preorder ι] {l : Filter α} {s : ι → Set α}
    (hs : l.HasAntitoneBasis s) (i : ι) : s i ∈ l :=
  hs.toHasBasis.mem_of_mem trivial

Membership of Basis Sets in Filter with Antitone Basis

Informal description

Let $\alpha$ be a type, $\iota$ be a preorder, $l$ be a filter on $\alpha$, and $s : \iota \to \text{Set} \alpha$ be an antitone basis for $l$. Then for any index $i \in \iota$, the set $s(i)$ belongs to the filter $l$.

Filter.HasAntitoneBasis.hasBasis_ge theorem

 [Preorder ι] [IsDirected ι (· ≤ ·)] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) (i : ι) :
  l.HasBasis (fun j => i ≤ j) s

Full source

theorem HasAntitoneBasis.hasBasis_ge [Preorder ι] [IsDirected ι (· ≤ ·)] {l : Filter α}
    {s : ι → Set α} (hs : l.HasAntitoneBasis s) (i : ι) : l.HasBasis (fun j => i ≤ j) s :=
  hs.1.to_hasBasis (fun j _ => (exists_ge_ge i j).imp fun _k hk => ⟨hk.1, hs.2 hk.2⟩) fun j _ =>
    ⟨j, trivial, Subset.rfl⟩

Filter Basis Restriction to Indices Above a Given Index in an Antitone Basis

Informal description

Let $\alpha$ be a type, $\iota$ be a preorder with directed order $\leq$, $l$ be a filter on $\alpha$, and $s : \iota \to \text{Set} \alpha$ be an antitone basis for $l$. Then for any index $i \in \iota$, the filter $l$ has a basis consisting of the sets $s(j)$ for all indices $j \geq i$.

Filter.HasBasis.exists_antitone_subbasis theorem

 {f : Filter α} [h : f.IsCountablyGenerated] {p : ι' → Prop} {s : ι' → Set α} (hs : f.HasBasis p s) :
  ∃ x : ℕ → ι', (∀ i, p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i)

Full source

/-- If `f` is countably generated and `f.HasBasis p s`, then `f` admits a decreasing basis
enumerated by natural numbers such that all sets have the form `s i`. More precisely, there is a
sequence `i n` such that `p (i n)` for all `n` and `s (i n)` is a decreasing sequence of sets which
forms a basis of `f`. -/
theorem HasBasis.exists_antitone_subbasis {f : Filter α} [h : f.IsCountablyGenerated]
    {p : ι' → Prop} {s : ι' → Set α} (hs : f.HasBasis p s) :
    ∃ x : ℕ → ι', (∀ i, p (x i)) ∧ f.HasAntitoneBasis fun i => s (x i) := by
  obtain ⟨x', hx'⟩ : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i) := by
    rcases h with ⟨s, hsc, rfl⟩
    rw [generate_eq_biInf]
    exact countable_biInf_principal_eq_seq_iInf hsc
  have : ∀ i, x' i ∈ f := fun i => hx'.symm ▸ (iInf_le (fun i => 𝓟 (x' i)) i) (mem_principal_self _)
  let x : ℕ → { i : ι' // p i } := fun n =>
    Nat.recOn n (hs.index _ <| this 0) fun n xn =>
      hs.index _ <| inter_mem (this <| n + 1) (hs.mem_of_mem xn.2)
  have x_anti : Antitone fun i => s (x i).1 :=
    antitone_nat_of_succ_le fun i => (hs.set_index_subset _).trans inter_subset_right
  have x_subset : ∀ i, s (x i).1 ⊆ x' i := by
    rintro (_ | i)
    exacts [hs.set_index_subset _, (hs.set_index_subset _).trans inter_subset_left]
  refine ⟨fun i => (x i).1, fun i => (x i).2, ?_⟩
  have : (⨅ i, 𝓟 (s (x i).1)).HasAntitoneBasis fun i => s (x i).1 := .iInf_principal x_anti
  convert this
  exact
    le_antisymm (le_iInf fun i => le_principal_iff.2 <| by cases i <;> apply hs.set_index_mem)
      (hx'.symm ▸
        le_iInf fun i => le_principal_iff.2 <| this.1.mem_iff.2 ⟨i, trivial, x_subset i⟩)

Existence of Antitone Subbasis for Countably Generated Filters with Basis

Informal description

Let $f$ be a countably generated filter on a type $\alpha$ with a basis consisting of sets $s_i$ indexed by a predicate $p$. Then there exists a sequence of indices $(x_n)_{n \in \mathbb{N}}$ such that: 1. For every $n \in \mathbb{N}$, $p(x_n)$ holds. 2. The filter $f$ has an antitone basis given by the sets $s_{x_n}$, i.e., the sequence $(s_{x_n})_{n \in \mathbb{N}}$ is decreasing and forms a basis for $f$.

Filter.exists_antitone_basis theorem

(f : Filter α) [f.IsCountablyGenerated] : ∃ x : ℕ → Set α, f.HasAntitoneBasis x

Full source

/-- A countably generated filter admits a basis formed by an antitone sequence of sets. -/
theorem exists_antitone_basis (f : Filter α) [f.IsCountablyGenerated] :
    ∃ x : ℕ → Set α, f.HasAntitoneBasis x :=
  let ⟨x, _, hx⟩ := f.basis_sets.exists_antitone_subbasis
  ⟨x, hx⟩

Existence of Antitone Basis for Countably Generated Filters

Informal description

For any countably generated filter $f$ on a type $\alpha$, there exists a decreasing sequence of sets $(x_n)_{n \in \mathbb{N}}$ such that $x_n$ forms an antitone basis for $f$. That is, the sequence $(x_n)$ is decreasing (i.e., $x_{n+1} \subseteq x_n$ for all $n$) and a set $s$ belongs to $f$ if and only if it contains some $x_n$.

Filter.exists_antitone_seq theorem

(f : Filter α) [f.IsCountablyGenerated] : ∃ x : ℕ → Set α, Antitone x ∧ ∀ {s}, s ∈ f ↔ ∃ i, x i ⊆ s

Full source

theorem exists_antitone_seq (f : Filter α) [f.IsCountablyGenerated] :
    ∃ x : ℕ → Set α, Antitone x ∧ ∀ {s}, s ∈ f ↔ ∃ i, x i ⊆ s :=
  let ⟨x, hx⟩ := f.exists_antitone_basis
  ⟨x, hx.antitone, by simp [hx.1.mem_iff]⟩

Existence of Decreasing Sequence Basis for Countably Generated Filters

Informal description

For any countably generated filter $f$ on a type $\alpha$, there exists a decreasing sequence of sets $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ such that a set $s$ belongs to $f$ if and only if $s$ contains some $x_n$.

Filter.Inf.isCountablyGenerated instance

(f g : Filter α) [IsCountablyGenerated f] [IsCountablyGenerated g] : IsCountablyGenerated (f ⊓ g)

Full source

instance Inf.isCountablyGenerated (f g : Filter α) [IsCountablyGenerated f]
    [IsCountablyGenerated g] : IsCountablyGenerated (f ⊓ g) := by
  rcases f.exists_antitone_basis with ⟨s, hs⟩
  rcases g.exists_antitone_basis with ⟨t, ht⟩
  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.inf ht.1, Set.to_countable _⟩

Countable Generation of Filter Infima

Informal description

For any two countably generated filters $f$ and $g$ on a type $\alpha$, their infimum $f \sqcap g$ is also countably generated.

Filter.map.isCountablyGenerated instance

(l : Filter α) [l.IsCountablyGenerated] (f : α → β) : (map f l).IsCountablyGenerated

Full source

instance map.isCountablyGenerated (l : Filter α) [l.IsCountablyGenerated] (f : α → β) :
    (map f l).IsCountablyGenerated :=
  let ⟨_x, hxl⟩ := l.exists_antitone_basis
  (hxl.map _).isCountablyGenerated

Countable Generation of Image Filters

Informal description

For any countably generated filter $l$ on a type $\alpha$ and any function $f : \alpha \to \beta$, the image filter $\text{map}\,f\,l$ on $\beta$ is also countably generated.

Filter.comap.isCountablyGenerated instance

(l : Filter β) [l.IsCountablyGenerated] (f : α → β) : (comap f l).IsCountablyGenerated

Full source

instance comap.isCountablyGenerated (l : Filter β) [l.IsCountablyGenerated] (f : α → β) :
    (comap f l).IsCountablyGenerated :=
  let ⟨_x, hxl⟩ := l.exists_antitone_basis
  (hxl.comap _).isCountablyGenerated

Countable Generation of Preimage Filters

Informal description

For any countably generated filter $l$ on a type $\beta$ and any function $f : \alpha \to \beta$, the preimage filter $\text{comap}\,f\,l$ on $\alpha$ is also countably generated.

Filter.Sup.isCountablyGenerated instance

(f g : Filter α) [IsCountablyGenerated f] [IsCountablyGenerated g] : IsCountablyGenerated (f ⊔ g)

Full source

instance Sup.isCountablyGenerated (f g : Filter α) [IsCountablyGenerated f]
    [IsCountablyGenerated g] : IsCountablyGenerated (f ⊔ g) := by
  rcases f.exists_antitone_basis with ⟨s, hs⟩
  rcases g.exists_antitone_basis with ⟨t, ht⟩
  exact HasCountableBasis.isCountablyGenerated ⟨hs.1.sup ht.1, Set.to_countable _⟩

Countable Generation of Supremum of Filters

Informal description

For any two countably generated filters $f$ and $g$ on a type $\alpha$, their supremum $f \sqcup g$ is also countably generated.

Filter.prod.isCountablyGenerated instance

 (la : Filter α) (lb : Filter β) [IsCountablyGenerated la] [IsCountablyGenerated lb] : IsCountablyGenerated (la ×ˢ lb)

Full source

instance prod.isCountablyGenerated (la : Filter α) (lb : Filter β) [IsCountablyGenerated la]
    [IsCountablyGenerated lb] : IsCountablyGenerated (la ×ˢ lb) :=
  Filter.Inf.isCountablyGenerated _ _

Countable Generation of Product Filters

Informal description

For any two countably generated filters $F$ on type $\alpha$ and $G$ on type $\beta$, their product filter $F \times^s G$ on $\alpha \times \beta$ is also countably generated.

Filter.coprod.isCountablyGenerated instance

 (la : Filter α) (lb : Filter β) [IsCountablyGenerated la] [IsCountablyGenerated lb] :
  IsCountablyGenerated (la.coprod lb)

Full source

instance coprod.isCountablyGenerated (la : Filter α) (lb : Filter β) [IsCountablyGenerated la]
    [IsCountablyGenerated lb] : IsCountablyGenerated (la.coprod lb) :=
  Filter.Sup.isCountablyGenerated _ _

Countable Generation of Coproduct Filters

Informal description

For any countably generated filters $la$ on type $\alpha$ and $lb$ on type $\beta$, their coproduct filter $la.coprod\,lb$ on $\alpha \times \beta$ is also countably generated.

Filter.isCountablyGenerated_seq theorem

[Countable ι'] (x : ι' → Set α) : IsCountablyGenerated (⨅ i, 𝓟 (x i))

Full source

theorem isCountablyGenerated_seq [Countable ι'] (x : ι' → Set α) :
    IsCountablyGenerated (⨅ i, 𝓟 (x i)) := by
  use range x, countable_range x
  rw [generate_eq_biInf, iInf_range]

Countable Infimum of Principal Filters is Countably Generated

Informal description

For any countable type $\iota'$ and any family of sets $x \colon \iota' \to \mathcal{P}(\alpha)$, the infimum of the principal filters generated by the sets $x(i)$ is a countably generated filter. In other words, the filter $\bigsqcap_{i \in \iota'} \mathfrak{P}(x(i))$ is countably generated.

Filter.isCountablyGenerated_of_seq theorem

{f : Filter α} (h : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i)) : f.IsCountablyGenerated

Full source

theorem isCountablyGenerated_of_seq {f : Filter α} (h : ∃ x : ℕ → Set α, f = ⨅ i, 𝓟 (x i)) :
    f.IsCountablyGenerated := by
  rcases h with ⟨x, rfl⟩
  apply isCountablyGenerated_seq

Countable generation of filters via sequences

Informal description

For any filter $f$ on a type $\alpha$, if there exists a sequence of sets $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $f$ is equal to the infimum of the principal filters generated by the $x_n$, then $f$ is countably generated.

Filter.isCountablyGenerated_biInf_principal theorem

{B : Set (Set α)} (h : B.Countable) : IsCountablyGenerated (⨅ s ∈ B, 𝓟 s)

Full source

theorem isCountablyGenerated_biInf_principal {B : Set (Set α)} (h : B.Countable) :
    IsCountablyGenerated (⨅ s ∈ B, 𝓟 s) :=
  isCountablyGenerated_of_seq (countable_biInf_principal_eq_seq_iInf h)

Countable Infimum of Principal Filters is Countably Generated

Informal description

For any countable collection of sets $B$ in a type $\alpha$, the infimum of the principal filters generated by the sets in $B$ is a countably generated filter. That is, the filter $\bigsqcap_{s \in B} \mathfrak{P}(s)$ is countably generated, where $\mathfrak{P}(s)$ denotes the principal filter generated by $s$.

Filter.isCountablyGenerated_iff_exists_antitone_basis theorem

{f : Filter α} : IsCountablyGenerated f ↔ ∃ x : ℕ → Set α, f.HasAntitoneBasis x

Full source

theorem isCountablyGenerated_iff_exists_antitone_basis {f : Filter α} :
    IsCountablyGeneratedIsCountablyGenerated f ↔ ∃ x : ℕ → Set α, f.HasAntitoneBasis x := by
  constructor
  · intro h
    exact f.exists_antitone_basis
  · rintro ⟨x, h⟩
    rw [h.1.eq_iInf]
    exact isCountablyGenerated_seq x

Characterization of Countably Generated Filters via Antitone Bases

Informal description

A filter $f$ on a type $\alpha$ is countably generated if and only if there exists a decreasing sequence of sets $(x_n)_{n \in \mathbb{N}}$ in $\alpha$ such that $x_n$ forms an antitone basis for $f$. That is, a set $s$ belongs to $f$ if and only if it contains some $x_n$, and $x_{n+1} \subseteq x_n$ for all $n \in \mathbb{N}$.

Filter.isCountablyGenerated_principal theorem

(s : Set α) : IsCountablyGenerated (𝓟 s)

Full source

@[instance]
theorem isCountablyGenerated_principal (s : Set α) : IsCountablyGenerated (𝓟 s) :=
  isCountablyGenerated_of_seq ⟨fun _ => s, iInf_const.symm⟩

Countable Generation of Principal Filters

Informal description

For any set $s$ in a type $\alpha$, the principal filter $\mathfrak{P}(s)$ generated by $s$ is countably generated.

Filter.isCountablyGenerated_pure theorem

(a : α) : IsCountablyGenerated (pure a)

Full source

@[instance]
theorem isCountablyGenerated_pure (a : α) : IsCountablyGenerated (pure a) := by
  rw [← principal_singleton]
  exact isCountablyGenerated_principal _

Pure Filters are Countably Generated

Informal description

For any element $a$ of a type $\alpha$, the pure filter at $a$ (i.e., the collection of all subsets of $\alpha$ containing $a$) is countably generated.

Filter.isCountablyGenerated_bot theorem

: IsCountablyGenerated (⊥ : Filter α)

Full source

@[instance]
theorem isCountablyGenerated_bot : IsCountablyGenerated (⊥ : Filter α) :=
  @principal_empty α ▸ isCountablyGenerated_principal _

Countable Generation of the Bottom Filter

Informal description

The bottom filter $\bot$ on a type $\alpha$ is countably generated.

Filter.isCountablyGenerated_top theorem

: IsCountablyGenerated (⊤ : Filter α)

Full source

@[instance]
theorem isCountablyGenerated_top : IsCountablyGenerated (⊤ : Filter α) :=
  @principal_univ α ▸ isCountablyGenerated_principal _

Countable Generation of the Top Filter

Informal description

The top filter $\top$ on a type $\alpha$ (i.e., the filter containing all subsets of $\alpha$) is countably generated.

Filter.iInf.isCountablyGenerated instance

 {ι : Sort*} {α : Type*} [Countable ι] (f : ι → Filter α) [∀ i, IsCountablyGenerated (f i)] :
  IsCountablyGenerated (⨅ i, f i)

Full source

instance iInf.isCountablyGenerated {ι : Sort*} {α : Type*} [Countable ι] (f : ι → Filter α)
    [∀ i, IsCountablyGenerated (f i)] : IsCountablyGenerated (⨅ i, f i) := by
  choose s hs using fun i => exists_antitone_basis (f i)
  rw [← PLift.down_surjective.iInf_comp]
  refine HasCountableBasis.isCountablyGenerated ⟨hasBasis_iInf fun n => (hs _).1, ?_⟩
  refine (countable_range <| Sigma.map ((↑) : Finset (PLift ι) → Set (PLift ι)) fun _ => id).mono ?_
  rintro ⟨I, f⟩ ⟨hI, -⟩
  lift I to Finset (PLift ι) using hI
  exact ⟨⟨I, f⟩, rfl⟩

Countable Infimum of Countably Generated Filters is Countably Generated

Informal description

For any countable type $\iota$ and any family of countably generated filters $(f_i)_{i \in \iota}$ on a type $\alpha$, the infimum filter $\bigsqcap_{i \in \iota} f_i$ is also countably generated.

Filter.pi.isCountablyGenerated instance

 {ι : Type*} {α : ι → Type*} [Countable ι] (f : ∀ i, Filter (α i)) [∀ i, IsCountablyGenerated (f i)] :
  IsCountablyGenerated (pi f)

Full source

instance pi.isCountablyGenerated {ι : Type*} {α : ι → Type*} [Countable ι]
    (f : ∀ i, Filter (α i)) [∀ i, IsCountablyGenerated (f i)] : IsCountablyGenerated (pi f) :=
  iInf.isCountablyGenerated _

Countable Generation of Pi Filters

Informal description

For any countable index type $\iota$ and any family of countably generated filters $(f_i)_{i \in \iota}$ on types $(\alpha_i)_{i \in \iota}$, the pi filter $\text{Filter.pi } f$ on the product type $\forall i, \alpha_i$ is also countably generated.