Projection_from_Product_Topology_is_Continuous
Provedcontinuous-mappingsprojection-from-product-topology-is-open-and-continuousprojectionsproofwikitychonoff-topology
Let and be topological spaces. Let be the product space of and , where is the Tychonoff topology on . Let and be the first and second projections from onto its factors. Then both and are are continuous.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Projection_from_Product_Topology_is_Continuous {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] : Continuous (Prod.fst : α × β → α) ∧ Continuous (Prod.snd : α × β → β) := by sorrySource