English
If f: X → Y and g: Z → W are open quotient maps, then Prod.map f g is an open quotient map.
Русский
Если f: X → Y и g: Z → W — открытые фактор-отображения, то Prod.map f g — открытое фактор-отображение.
LaTeX
$$$\IsOpenQuotientMap f \land \IsOpenQuotientMap g \Rightarrow \IsOpenQuotientMap(\mathrm{Prod.map} f g)$$$
Lean4
theorem prodMap {f : X → Y} {g : Z → W} (hf : IsOpenQuotientMap f) (hg : IsOpenQuotientMap g) :
IsOpenQuotientMap (Prod.map f g) :=
⟨.prodMap hf.1 hg.1, .prodMap hf.2 hg.2, .prodMap hf.3 hg.3⟩
-- Homeomorphisms between the various product: products of two homeomorphisms,
-- as well as commutativity and associativity. See below for the analogous results for sums,
-- as well as distributivity, etc.
