English
For a family s : ι → Set α, the infimum of the principal filters 𝓟(s_i) over i has a basis indexed by finite sets t ⊆ ι, given by the intersections ⋂_{i∈t} s_i.
Русский
Для семейства s_i множеств на α пределом по отношению к фильтрам является инфимум принципиальных фильтров 𝓟( s_i ) и имеет базис, индексированный конечными подмножествами t ⊆ ι, состоящий из пересечений ⋂_{i∈t} s_i.
LaTeX
$$$(\bigwedge_{i} \mathcal{P}(s_i)).HasBasis (\lambda t: Set\,ι. t.Finite) (\lambda t. \bigcap_{i \in t} s_i).$$$
Lean4
/-- If `s : ι → Set α` is an indexed family of sets, then finite intersections of `s i` form a basis
of `⨅ i, 𝓟 (s i)`. -/
theorem hasBasis_iInf_principal_finite {ι : Type*} (s : ι → Set α) :
(⨅ i, 𝓟 (s i)).HasBasis (fun t : Set ι => t.Finite) fun t => ⋂ i ∈ t, s i :=
by
refine ⟨fun U => (mem_iInf_finite _).trans ?_⟩
simp only [iInf_principal_finset, mem_principal, exists_finite_iff_finset, Finset.set_biInter_coe]
