English
If the topologies on X and Y are generated by families s and t, and ⋃ s = univ and ⋃ t = univ, then the product topology on X × Y is generated by the family { s × t | s ∈ s, t ∈ t }.
Русский
Если топологии на X и Y генерируются семьями s и t соответственно, и ⋃ s = Univ, ⋃ t = Univ, то произведение X×Y имеет топологию, порождаемую семейством { s × t | s ∈ s, t ∈ t }.
LaTeX
$$$$\text{If }\mathcal T_X = \mathrm{generateFrom}(s),\ \mathcal T_Y = \mathrm{generateFrom}(t),\ \bigcup s = \mathsf{univ},\ \bigcup t = \mathsf{univ},\ \mathcal T_{X\times Y} = \mathrm{generateFrom}(\{ s\times t \mid s \in s,\ t \in t\}).$$$$
Lean4
theorem prod_generateFrom_generateFrom_eq {X Y : Type*} {s : Set (Set X)} {t : Set (Set Y)} (hs : ⋃₀ s = univ)
(ht : ⋃₀ t = univ) :
@instTopologicalSpaceProd X Y (generateFrom s) (generateFrom t) = generateFrom (image2 (· ×ˢ ·) s t) :=
let G := generateFrom (image2 (· ×ˢ ·) s t)
le_antisymm
(le_generateFrom fun _ ⟨_, hu, _, hv, g_eq⟩ =>
g_eq.symm ▸
@IsOpen.prod _ _ (generateFrom s) (generateFrom t) _ _ (GenerateOpen.basic _ hu) (GenerateOpen.basic _ hv))
(le_inf
(coinduced_le_iff_le_induced.mp <|
le_generateFrom fun u hu =>
have : ⋃ v ∈ t, u ×ˢ v = Prod.fst ⁻¹' u := by simp_rw [← prod_iUnion, ← sUnion_eq_biUnion, ht, prod_univ]
show G.IsOpen (Prod.fst ⁻¹' u) by
rw [← this]
exact isOpen_iUnion fun v => isOpen_iUnion fun hv => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩)
(coinduced_le_iff_le_induced.mp <|
le_generateFrom fun v hv =>
have : ⋃ u ∈ s, u ×ˢ v = Prod.snd ⁻¹' v := by
simp_rw [← iUnion_prod_const, ← sUnion_eq_biUnion, hs, univ_prod]
show G.IsOpen (Prod.snd ⁻¹' v) by
rw [← this]
exact isOpen_iUnion fun u => isOpen_iUnion fun hu => GenerateOpen.basic _ ⟨_, hu, _, hv, rfl⟩))
