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.

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.

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.

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.

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.

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

Equations

• Filter.Nat.inhabitedCountableFilterBasis = { default := { toFilterBasis := default, countable := Filter.Nat.inhabitedCountableFilterBasis.proof_1 } }

theorem Filter.HasCountableBasis.isCountablyGenerated {α : Type u_1} {ι : Type u_4} {f : Filter α} {p : ι → Prop} {s : ι → Set α} (h : f.HasCountableBasis p s) : f.IsCountablyGenerated

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

theorem Filter.antitone_seq_of_seq {α : Type u_1} (s : ℕ → Set α) : ∃ (t : ℕ → Set α), Antitone t ∧ ⨅ (i : ℕ), principal (s i) = ⨅ (i : ℕ), principal (t i)

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)

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)

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)

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

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

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

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

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.

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

instance Filter.Inf.isCountablyGenerated {α : Type u_1} (f g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated] : (f ⊓ g).IsCountablyGenerated

instance Filter.map.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter α) [l.IsCountablyGenerated] (f : α → β) : (map f l).IsCountablyGenerated

instance Filter.comap.isCountablyGenerated {α : Type u_1} {β : Type u_2} (l : Filter β) [l.IsCountablyGenerated] (f : α → β) : (comap f l).IsCountablyGenerated

instance Filter.Sup.isCountablyGenerated {α : Type u_1} (f g : Filter α) [f.IsCountablyGenerated] [g.IsCountablyGenerated] : (f ⊔ g).IsCountablyGenerated

instance Filter.prod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated] : (la ×ˢ lb).IsCountablyGenerated

instance Filter.coprod.isCountablyGenerated {α : Type u_1} {β : Type u_2} (la : Filter α) (lb : Filter β) [la.IsCountablyGenerated] [lb.IsCountablyGenerated] : (la.coprod lb).IsCountablyGenerated

theorem Filter.isCountablyGenerated_seq {α : Type u_1} {ι' : Sort u_5} [Countable ι'] (x : ι' → Set α) : (⨅ (i : ι'), principal (x i)).IsCountablyGenerated

theorem Filter.isCountablyGenerated_of_seq {α : Type u_1} {f : Filter α} (h : ∃ (x : ℕ → Set α), f = ⨅ (i : ℕ), principal (x i)) : f.IsCountablyGenerated

theorem Filter.isCountablyGenerated_biInf_principal {α : Type u_1} {B : Set (Set α)} (h : B.Countable) : (⨅ s ∈ B, principal s).IsCountablyGenerated

theorem Filter.isCountablyGenerated_iff_exists_antitone_basis {α : Type u_1} {f : Filter α} : f.IsCountablyGenerated ↔ ∃ (x : ℕ → Set α), f.HasAntitoneBasis x

instance Filter.isCountablyGenerated_principal {α : Type u_1} (s : Set α) : (principal s).IsCountablyGenerated

instance Filter.isCountablyGenerated_pure {α : Type u_1} (a : α) : (pure a).IsCountablyGenerated

instance Filter.isCountablyGenerated_bot {α : Type u_1} : ⊥.IsCountablyGenerated

instance Filter.isCountablyGenerated_top {α : Type u_1} : ⊤.IsCountablyGenerated

instance Filter.iInf.isCountablyGenerated {ι : Sort u} {α : Type v} [Countable ι] (f : ι → Filter α) [∀ (i : ι), (f i).IsCountablyGenerated] : (⨅ (i : ι), f i).IsCountablyGenerated

instance Filter.pi.isCountablyGenerated {ι : Type u_6} {α : ι → Type u_7} [Countable ι] (f : (i : ι) → Filter (α i)) [∀ (i : ι), (f i).IsCountablyGenerated] : (pi f).IsCountablyGenerated