English
For a family of spaces X_i, the Pi-type basis is given by a family of sets whose elements are finite intersections over i of sets U_i, matching the standard basis through a product construction.
Русский
Для семейства пространств X_i базис Пи определяется через множество, состоящее из конечных пересечений по i множеств U_i, соответствующее базису произведения.
LaTeX
$$$\\mathsf{isTopologicalBasis\_pi}\\;{\\iota}:\\; \\text{(isTopologicalBasis)}$$$
Lean4
theorem isTopologicalBasis_pi {ι : Type*} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] {T : ∀ i, Set (Set (X i))}
(cond : ∀ i, IsTopologicalBasis (T i)) :
IsTopologicalBasis {S | ∃ (U : ∀ i, Set (X i)) (F : Finset ι), (∀ i, i ∈ F → U i ∈ T i) ∧ S = (F : Set ι).pi U} :=
by simpa only [Set.pi_def] using IsTopologicalBasis.iInf_induced cond eval
