English
The indexed product of a possibly infinite family of pure filters has a basis given by finite cylinders.
Русский
Произведение по индексу возможно бесконечно, имеет базис в виде цилиндров с конечной поддержкой.
LaTeX
$$$\text{HasBasis}(\pi i, pure(f_i)) \text{ with finite cylinders}$$$
Lean4
/-- The indexed product of a (possibly, infinite) family of pure filters `pure (f i)`
is generated by the sets of functions that are equal to `f` on a finite set.
If the index type is finite, then the indexed product of pure filters is a pure filter,
see `pi_pure`. -/
theorem hasBasis_pi_pure (f : (i : ι) → α i) :
HasBasis (pi fun i ↦ pure (f i)) Set.Finite (fun I ↦ {g | ∀ i ∈ I, g i = f i}) :=
⟨fun _ ↦ mem_pi_pure⟩
