English
The family {cylinder(x,n)} forms a topological basis for the product topology.
Русский
Семейство цилиндров {cylinder(x,n)} образует топологический базис произведения.
LaTeX
$$$$ IsTopologicalBasis\{ s:\ Set((n\ mapsto E_n)) \mid \exists x,n, s = cylinder(x,n) \} $$$$
Lean4
theorem isTopologicalBasis_cylinders :
IsTopologicalBasis {s : Set (∀ n, E n) | ∃ (x : ∀ n, E n) (n : ℕ), s = cylinder x n} :=
by
apply isTopologicalBasis_of_isOpen_of_nhds
· rintro u ⟨x, n, rfl⟩
apply isOpen_cylinder
· intro x u hx u_open
obtain ⟨v, ⟨U, F, -, rfl⟩, xU, Uu⟩ :
∃
v ∈
{S : Set (∀ i : ℕ, E i) |
∃ (U : ∀ i : ℕ, Set (E i)) (F : Finset ℕ),
(∀ i : ℕ, i ∈ F → U i ∈ {s : Set (E i) | IsOpen s}) ∧ S = (F : Set ℕ).pi U},
x ∈ v ∧ v ⊆ u :=
(isTopologicalBasis_pi fun n : ℕ => isTopologicalBasis_opens).exists_subset_of_mem_open hx u_open
rcases Finset.bddAbove F with ⟨n, hn⟩
refine ⟨cylinder x (n + 1), ⟨x, n + 1, rfl⟩, self_mem_cylinder _ _, Subset.trans ?_ Uu⟩
intro y hy
suffices ∀ i : ℕ, i ∈ F → y i ∈ U i by simpa
intro i hi
have : y i = x i := mem_cylinder_iff.1 hy i ((hn hi).trans_lt (lt_add_one n))
rw [this]
simp only [Set.mem_pi, Finset.mem_coe] at xU
exact xU i hi
