Continuous_Mapping_is_Continuous_on_Induced_Topological_Spaces
Provedcontinuous-mappingsmetric-spacesproofwikitopology
Let and be metric spaces. Let and be the topologies induced by the metrics and . Let and be the resulting topological spaces. Let be a mapping. Then is -continuous is -continuous.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Continuous_Mapping_is_Continuous_on_Induced_Topological_Spaces {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s : Set α) (hf : Continuous f) : ContinuousOn f s := by sorrySource