From e33e62c2044c7089d2c0f9b487e4f02ad00630e8 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sat, 12 Sep 2026 13:56:10 -0500 Subject: [PATCH 1/2] feat: add `Filter.HasBasis.iInf_of_finite` --- Mathlib/Order/Filter/Bases/Finite.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Mathlib/Order/Filter/Bases/Finite.lean b/Mathlib/Order/Filter/Bases/Finite.lean index a6ca2f84864196..2262abdfb5348b 100644 --- a/Mathlib/Order/Filter/Bases/Finite.lean +++ b/Mathlib/Order/Filter/Bases/Finite.lean @@ -85,6 +85,26 @@ protected theorem HasBasis.iInf {ι : Type*} {ι' : ι → Type*} {l : ι → Fi cases hI.nonempty_fintype exact iInter_mem.2 fun i => mem_iInf_of_mem ↑i <| (hl i).mem_of_mem <| hf _ +/-- When the indexing type is finite, `⨅ i, l i` has a basis consisting of intersections of sets +from bases of each `l i`. -/ +theorem HasBasis.iInf_of_finite {ι : Type*} {ι' : ι → Type*} [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, s i (f i) := by + refine ⟨fun t ↦ ⟨fun ht ↦ ?_, fun ⟨f, hf, hsub⟩ ↦ ?_⟩⟩ + · obtain ⟨u, hu, rfl⟩ := (mem_iInf_of_finite t).1 ht + choose f hf hsub using fun i ↦ (hl i).mem_iff.1 (hu i) + exact ⟨f, hf, iInter_mono hsub⟩ + · exact mem_of_superset (iInter_mem.2 fun i ↦ mem_iInf_of_mem i <| (hl i).mem_of_mem (hf i)) hsub + +theorem HasBasis.biInf_of_finset {ι : Type*} {ι' : ι → Type*} (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, s i (f i) := by + rw [iInf_subtype'] + exact HasBasis.iInf_of_finite fun i : I ↦ hl i i.2 + open scoped Function in -- required for scoped `on` notation theorem _root_.Pairwise.exists_mem_filter_basis_of_disjoint {I} [Finite I] {l : I → Filter α} {ι : I → Sort*} {p : ∀ i, ι i → Prop} {s : ∀ i, ι i → Set α} (hd : Pairwise (Disjoint on l)) From b34949fee51664ba45e6e50f7d21caa708409b57 Mon Sep 17 00:00:00 2001 From: Jireh Loreaux Date: Sun, 13 Sep 2026 20:55:48 -0500 Subject: [PATCH 2/2] Update Mathlib/Order/Filter/Bases/Finite.lean Co-authored-by: Bhavik Mehta --- Mathlib/Order/Filter/Bases/Finite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/Filter/Bases/Finite.lean b/Mathlib/Order/Filter/Bases/Finite.lean index 2262abdfb5348b..157ce7b261eb67 100644 --- a/Mathlib/Order/Filter/Bases/Finite.lean +++ b/Mathlib/Order/Filter/Bases/Finite.lean @@ -97,7 +97,7 @@ theorem HasBasis.iInf_of_finite {ι : Type*} {ι' : ι → Type*} [Finite ι] exact ⟨f, hf, iInter_mono hsub⟩ · exact mem_of_superset (iInter_mem.2 fun i ↦ mem_iInf_of_mem i <| (hl i).mem_of_mem (hf i)) hsub -theorem HasBasis.biInf_of_finset {ι : Type*} {ι' : ι → Type*} (I : Finset ι) +theorem HasBasis.biInf_finset {ι : Type*} {ι' : ι → Type*} (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))