English
The product topology on X × Y is generated by the family of rectangles s × t with s, t open in X and Y, respectively.
Русский
Топология произведения X × Y порождается множеством прямоугольников s × t, где s и t открыты в X и Y соответственно.
LaTeX
$$$$\mathrm{Top}_{X\times Y} = \mathrm{generateFrom}\bigl\{ s\times t \mid s \in \mathcal O_X,\ t \in \mathcal O_Y\bigr\}.$$$$
Lean4
theorem prod_eq_generateFrom :
instTopologicalSpaceProd = generateFrom {g | ∃ (s : Set X) (t : Set Y), IsOpen s ∧ IsOpen t ∧ g = s ×ˢ t} :=
le_antisymm (le_generateFrom fun _ ⟨_, _, hs, ht, g_eq⟩ => g_eq.symm ▸ hs.prod ht)
(le_inf (forall_mem_image.2 fun t ht => GenerateOpen.basic _ ⟨t, univ, by simpa [Set.prod_eq] using ht⟩)
(forall_mem_image.2 fun t ht => GenerateOpen.basic _ ⟨univ, t, by simpa [Set.prod_eq] using ht⟩))
-- TODO: align with `mem_nhds_prod_iff'`
