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

source
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
source
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 := ⋯ }

Instances For

source
theorem Filter.FilterBasis.ofSets_sets {α : Type u_1} (s : Set (Set α)) :
(ofSets s).sets = Set.sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s}
source
theorem Filter.generate_eq_generate_inter {α : Type u_1} (s : Set (Set α)) :
generate s = generate (Set.sInter '' {t : Set (Set α) | t.Finite ∧ t ⊆ s})
source
theorem Filter.ofSets_filter_eq_generate {α : Type u_1} (s : Set (Set α)) :
(FilterBasis.ofSets s).filter = generate s
source
theorem Filter.generate_neBot_iff {α : Type u_1} {s : Set (Set α)} :
(generate s).NeBot ↔ ∀ t ⊆ s, t.Finite → (⋂₀ t).Nonempty
source
theorem Filter.HasBasis.iInf' {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {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)
source
@[deprecated Filter.HasBasis.iInf' (since := "2025-05-05")]
theorem Filter.hasBasis_iInf' {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {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)

Alias of `Filter.HasBasis.iInf'`.

source
theorem Filter.HasBasis.iInf {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {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)
source
@[deprecated Filter.HasBasis.iInf (since := "2025-05-05")]
theorem Filter.hasBasis_iInf {α : Type u_1} {ι : Type u_6} {ι' : ι → Type u_7} {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)

Alias of `Filter.HasBasis.iInf`.

source
theorem Pairwise.exists_mem_filter_basis_of_disjoint {α : Type u_1} {I : Type u_7} [Finite I] {l : I → Filter α} {ι : I → Sort u_6} {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))
source
theorem Set.PairwiseDisjoint.exists_mem_filter_basis {α : Type u_1} {I : Type u_6} {l : I → Filter α} {ι : I → Sort u_7} {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)
source
theorem Filter.hasBasis_iInf_principal_finite {α : Type u_1} {ι : Type u_6} (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)`.