English
Let B1 be a topological basis for α and B2 a topological basis for β. Then the set of all products U × V with U ∈ B1 and V ∈ B2 forms a topological basis for the product space α × β.
Русский
Пусть B1 является топологическим базисом для пространства α, а B2 — для β. Тогда множество всех произведений U × V с U ∈ B1 и V ∈ B2 образует топологический базис для произведения α × β.
LaTeX
$$$\\mathsf{IsTopologicalBasis}(B_1) \\rightarrow \\mathsf{IsTopologicalBasis}(B_2) \\rightarrow \\mathsf{IsTopologicalBasis}\\left(\\{U \\times V : U \\in B_1,\\ V \\in B_2\\}\\right)$$$
Lean4
protected theorem prod {β} [TopologicalSpace β] {B₁ : Set (Set α)} {B₂ : Set (Set β)} (h₁ : IsTopologicalBasis B₁)
(h₂ : IsTopologicalBasis B₂) : IsTopologicalBasis (image2 (· ×ˢ ·) B₁ B₂) :=
h₁.inf_induced h₂ Prod.fst Prod.snd
