English
The infimum of a family of filters has a basis described by finite subsets of the index set and corresponding basis elements.
Русский
Пересечение большого множества фильтров имеет базис, описанный через конечные подмножества индексов и соответствующие элементы базиса.
LaTeX
$$HasBasis.iInf' describes an explicit basis for ⨅ i, l i with index If and sets ⋂ i∈If.1, s i (If.2 i).$$
Lean4
protected theorem iInf' {ι : Type*} {ι' : ι → Type*} {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) :=
⟨by
intro t
constructor
· simp only [mem_iInf', (hl _).mem_iff]
rintro ⟨I, hI, V, hV, -, rfl, -⟩
choose u hu using hV
exact ⟨⟨I, u⟩, ⟨hI, fun i _ => (hu i).1⟩, iInter₂_mono fun i _ => (hu i).2⟩
· rintro ⟨⟨I, f⟩, ⟨hI₁, hI₂⟩, hsub⟩
refine mem_of_superset ?_ hsub
exact (biInter_mem hI₁).mpr fun i hi => mem_iInf_of_mem i <| (hl i).mem_of_mem <| hI₂ _ hi⟩
