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_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)

@[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'.

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)

@[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.

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))

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)

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