Continuous_Mapping_to_Topological_Product
Provedcontinuous-mappingsproduct-spacesproofwiki
Let be a product space of two topological spaces and . Let and be the first and second projections from onto its factors. Let be a topological space. Let be a mapping. Then is continuous and are continuous.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Continuous_Mapping_to_Topological_Product {α : Type _} {β : Type _} {γ : Type _} [TopologicalSpace α] [TopologicalSpace β] [TopologicalSpace γ] (f : α → β) (g : α → γ) (hf : Continuous f) (hg : Continuous g) : Continuous (fun x => (f x, g x)) := by sorrySource