# Countably generated filters #

In this file we define a typeclass `Filter.IsCountablyGenerated` saying that a filter is generated by a countable family of sets.

We also define predicates `Filter.IsCountableBasis` and `Filter.HasCountableBasis` saying that a specific family of sets is a countable basis.

source
class Filter.IsCountablyGenerated {α : Type u_1} (f : Filter α) :
Prop

`IsCountablyGenerated f` means `f = generate s` for some countable `s`.

- out : ∃ (s : Set (Set α)), s.Countable ∧ f = generate s

  There exists a countable set that generates the filter.

Instances

source
structure Filter.IsCountableBasis {α : Type u_1} {ι : Type u_4} (p : ι → Prop) (s : ι → Set α) extends Filter.IsBasis p s :
Prop

`IsCountableBasis p s` means the image of `s` bounded by `p` is a countable filter basis.

- nonempty : ∃ (i : ι), p i
- inter {i j : ι} : p i → p j → ∃ (k : ι), p k ∧ s k ⊆ s i ∩ s j
- countable : (setOf p).Countable

  The set of `i` that satisfy the predicate `p` is countable.

Instances For

source
structure Filter.HasCountableBasis {α : Type u_1} {ι : Type u_4} (l : Filter α) (p : ι → Prop) (s : ι → Set α) extends l.HasBasis p s :
Prop

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.

- mem_iff' (t : Set α) : t ∈ l ↔ ∃ (i : ι), p i ∧ s i ⊆ t
- countable : (setOf p).Countable

  The set of `i` that satisfy the predicate `p` is countable.

Instances For

source
structure Filter.CountableFilterBasis (α : Type u_6) extends FilterBasis α :
Type u_6

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.

- sets : Set (Set α)
- nonempty : self.sets.Nonempty
- inter_sets {x y : Set α} : x ∈ self.sets → y ∈ self.sets → ∃ z ∈ self.sets, z ⊆ x ∩ y
- countable : self.sets.Countable

  The set of sets of the filter basis is countable.

Instances For

source
instance Filter.Nat.inhabitedCountableFilterBasis :
Inhabited (CountableFilterBasis ℕ)
Equations

- Filter.Nat.inhabitedCountableFilterBasis = { default := { toFilterBasis := default, countable := Filter.Nat.inhabitedCountableFilterBasis._proof_1 } }

source
theorem Filter.HasCountableBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_4} {f : Filter α} {p : ι → Prop} {s : ι → Set α} (h : f.HasCountableBasis p s) :
f.IsCountablyGenerated
source
theorem Filter.HasBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_4} [Countable ι] {f : Filter α} {p : ι → Prop} {s : ι → Set α} (h : f.HasBasis p s) :
f.IsCountablyGenerated
source
theorem Filter.antitone_seq_of_seq {α : Type u_1} (s : ℕ → Set α) :
∃ (t : ℕ → Set α), Antitone t ∧ ⨅ (i : ℕ), principal (s i) = ⨅ (i : ℕ), principal (t i)
source
theorem Filter.countable_biInf_eq_iInf_seq {α : Type u_1} {ι : Type u_4} [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (Bne : B.Nonempty) (f : ι → α) :
∃ (x : ℕ → ι), ⨅ t ∈ B, f t = ⨅ (i : ℕ), f (x i)
source
theorem Filter.countable_biInf_eq_iInf_seq' {α : Type u_1} {ι : Type u_4} [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable) (f : ι → α) {i₀ : ι} (h : f i₀ = ⊤) :
∃ (x : ℕ → ι), ⨅ t ∈ B, f t = ⨅ (i : ℕ), f (x i)
source
theorem Filter.countable_biInf_principal_eq_seq_iInf {α : Type u_1} {B : Set (Set α)} (Bcbl : B.Countable) :
∃ (x : ℕ → Set α), ⨅ t ∈ B, principal t = ⨅ (i : ℕ), principal (x i)
source
theorem Filter.HasAntitoneBasis.mem_iff {α : Type u_1} {ι : Type u_4} [Preorder ι] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) {t : Set α} :
t ∈ l ↔ ∃ (i : ι), s i ⊆ t
source
theorem Filter.HasAntitoneBasis.mem {α : Type u_1} {ι : Type u_4} [Preorder ι] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) (i : ι) :
s i ∈ l
source
theorem Filter.HasAntitoneBasis.hasBasis_ge {α : Type u_1} {ι : Type u_4} [Preorder ι] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {l : Filter α} {s : ι → Set α} (hs : l.HasAntitoneBasis s) (i : ι) :
l.HasBasis (fun (j : ι) => i ≤ j) s
source
theorem Filter.HasBasis.exists_antitone_subbasis {α : Type u_1} {ι' : Sort u_5} {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)

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

source
theorem Filter.exists_antitone_basis {α : Type u_1} (f : Filter α) [f.IsCountablyGenerated] :
∃ (x : ℕ → Set α), f.HasAntitoneBasis x

A countably generated filter admits a basis formed by an antitone sequence of sets.

source
theorem Filter.exists_antitone_seq {α : Type u_1} (f : Filter α) [f.IsCountablyGenerated] :
∃ (x : ℕ → Set α), Antitone x ∧ ∀ {s : Set α}, s ∈ f ↔ ∃ (i : ℕ), x i ⊆ s
source
instance Filter.Inf.isCountablyGenerated {α : Type u_1} (f g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated] :
(f ⊓ g).IsCountablyGenerated
source
instance Filter.map.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter α) [l.IsCountablyGenerated] (f : α → β) :
(map f l).IsCountablyGenerated
source
instance Filter.comap.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter β) [l.IsCountablyGenerated] (f : α → β) :
(comap f l).IsCountablyGenerated
source
instance Filter.Sup.isCountablyGenerated {α : Type u_1} (f g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated] :
(f ⊔ g).IsCountablyGenerated
source
instance Filter.prod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated] :
(la ×ˢ lb).IsCountablyGenerated
source
instance Filter.coprod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated] :
(la.coprod lb).IsCountablyGenerated
source
theorem Filter.isCountablyGenerated_seq {α : Type u_1} {ι' : Sort u_5} [Countable ι'] (x : ι' → Set α) :
(⨅ (i : ι'), principal (x i)).IsCountablyGenerated
source
theorem Filter.isCountablyGenerated_of_seq {α : Type u_1} {f : Filter α} (h : ∃ (x : ℕ → Set α), f = ⨅ (i : ℕ), principal (x i)) :
f.IsCountablyGenerated
source
theorem Filter.isCountablyGenerated_biInf_principal {α : Type u_1} {B : Set (Set α)} (h : B.Countable) :
(⨅ s ∈ B, principal s).IsCountablyGenerated
source
theorem Filter.isCountablyGenerated_iff_exists_antitone_basis {α : Type u_1} {f : Filter α} :
f.IsCountablyGenerated ↔ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x
source
instance Filter.isCountablyGenerated_principal {α : Type u_1} (s : Set α) :
(principal s).IsCountablyGenerated
source
instance Filter.isCountablyGenerated_pure {α : Type u_1} (a : α) :
(pure a).IsCountablyGenerated
source
instance Filter.isCountablyGenerated_bot {α : Type u_1} :
⊥.IsCountablyGenerated
source
instance Filter.isCountablyGenerated_top {α : Type u_1} :
⊤.IsCountablyGenerated
source
instance Filter.iInf.isCountablyGenerated {ι : Sort u_6} {α : Type u_7} [Countable ι] (f : ι → Filter α) [∀ (i : ι), (f i).IsCountablyGenerated] :
(⨅ (i : ι), f i).IsCountablyGenerated
source
instance Filter.pi.isCountablyGenerated {ι : Type u_6} {α : ι → Type u_7} [Countable ι] (f : (i : ι) → Filter (α i)) [∀ (i : ι), (f i).IsCountablyGenerated] :
(pi f).IsCountablyGenerated