Finiteness results on filter bases

A filter basis B : FilterBasis α on a type α is a nonempty collection of sets of α such that the intersection of two elements of this collection contains some element of the collection.

theorem Filter.hasBasis_generate {α : Type u_1} (s : Set (Set α)) : (generate s).HasBasis (fun (t : Set (Set α)) => t.Finite ∧ t ⊆ s) fun (t : Set (Set α)) => ⋂₀ t

def Filter.FilterBasis.ofSets {α : Type u_1} (s : Set (Set α)) : FilterBasis α

The smallest filter basis containing a given collection of sets.

Equations

• Filter.FilterBasis.ofSets s = { sets := Set.sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}, nonempty := ⋯, inter_sets := ⋯ }

theorem Filter.FilterBasis.ofSets_sets {α : Type u_1} (s : Set (Set α)) : (ofSets s).sets = Set.sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}

theorem Filter.generate_eq_generate_inter {α : Type u_1} (s : Set (Set α)) : generate s = generate (Set.sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s})

theorem Filter.ofSets_filter_eq_generate {α : Type u_1} (s : Set (Set α)) : (FilterBasis.ofSets s).filter = generate s

theorem Filter.generate_neBot_iff {α : Type u_1} {s : Set (Set α)} : (generate s).NeBot ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty

theorem Filter.HasBasis.iInf' {α : Type u_1} {ι : Type u_4} {ι' : ι → Type u_5} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) : (⨅ (i : ι), l i).HasBasis (fun (If : Set ι × ((i : ι) → ι' i)) => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun (If : Set ι × ((i : ι) → ι' i)) => ⋂ i ∈ If.1, s i (If.2 i)

theorem Filter.HasBasis.iInf {α : Type u_1} {ι : Type u_4} {ι' : ι → Type u_5} {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) : (⨅ (i : ι), l i).HasBasis (fun (If : (I : Set ι) × ((i : ↑I) → ι' ↑i)) => If.fst.Finite ∧ ∀ (i : ↑If.fst), p (↑i) (If.snd i)) fun (If : (I : Set ι) × ((i : ↑I) → ι' ↑i)) => ⋂ (i : ↑If.fst), s (↑i) (If.snd i)

theorem Filter.HasBasis.iInf_of_finite {α : Type u_1} {ι : Type u_4} {ι' : ι → Type u_5} [Finite ι] {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ (i : ι), (l i).HasBasis (p i) (s i)) : (⨅ (i : ι), l i).HasBasis (fun (f : (i : ι) → ι' i) => ∀ (i : ι), p i (f i)) fun (f : (i : ι) → ι' i) => ⋂ (i : ι), s i (f i)

When the indexing type is finite, ⨅ i, l i has a basis consisting of intersections of sets from bases of each l i.

theorem Filter.HasBasis.biInf_finset {α : Type u_1} {ι : Type u_4} {ι' : ι → Type u_5} (I : Finset ι) {l : ι → Filter α} {p : (i : ι) → ι' i → Prop} {s : (i : ι) → ι' i → Set α} (hl : ∀ i ∈ I, (l i).HasBasis (p i) (s i)) : (⨅ i ∈ I, l i).HasBasis (fun (f : (i : ↥I) → ι' ↑i) => ∀ (i : ↥I), p (↑i) (f i)) fun (f : (i : ↥I) → ι' ↑i) => ⋂ (i : ↥I), s (↑i) (f i)

theorem Pairwise.exists_mem_filter_basis_of_disjoint {α : Type u_1} {I : Type u_5} [Finite I] {l : I → Filter α} {ι : I → Sort u_4} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} (hd : Pairwise (Function.onFun Disjoint l)) (h : ∀ (i : I), (l i).HasBasis (p i) (s i)) : ∃ (ind : (i : I) → ι i), (∀ (i : I), p i (ind i)) ∧ Pairwise (Function.onFun Disjoint fun (i : I) => s i (ind i))

theorem Set.PairwiseDisjoint.exists_mem_filter_basis {α : Type u_1} {I : Type u_4} {l : I → Filter α} {ι : I → Sort u_5} {p : (i : I) → ι i → Prop} {s : (i : I) → ι i → Set α} {S : Set I} (hd : S.PairwiseDisjoint l) (hS : S.Finite) (h : ∀ (i : I), (l i).HasBasis (p i) (s i)) : ∃ (ind : (i : I) → ι i), (∀ (i : I), p i (ind i)) ∧ S.PairwiseDisjoint fun (i : I) => s i (ind i)

theorem Filter.hasBasis_iInf_principal_finite {α : Type u_1} {ι : Type u_4} (s : ι → Set α) : (⨅ (i : ι), principal (s i)).HasBasis (fun (t : Set ι) => t.Finite) fun (t : Set ι) => ⋂ i ∈ t, s i

If s : ι → Set α is an indexed family of sets, then finite intersections of s i form a basis of ⨅ i, 𝓟 (s i).