English
If each f i has a basis, then pi f has a basis given by combinations of finite index sets and the corresponding p-conditions.
Русский
Если для каждого i фильтр f i имеет базис, то произведение pi f имеет базис, задаваемый парами конечного множества и условий p.
LaTeX
$$$\text{If } (f_i) \text{ has basis } (p_i) (s_i), \text{ then } (\pi f) \text{ has basis } (\lambda I, pI) ...$$$
Lean4
theorem hasBasis_pi {ι' : ι → Type*} {s : ∀ i, ι' i → Set (α i)} {p : ∀ i, ι' i → Prop}
(h : ∀ i, (f i).HasBasis (p i) (s i)) :
(pi f).HasBasis (fun If : Set ι × ∀ i, ι' i => If.1.Finite ∧ ∀ i ∈ If.1, p i (If.2 i)) fun If : Set ι × ∀ i, ι' i =>
If.1.pi fun i => s i <| If.2 i :=
by simpa [Set.pi_def] using HasBasis.iInf' fun i => (h i).comap (eval i : (∀ j, α j) → α i)
