Continuity_of_Composite_with_Inclusion
Provedcomposite-mappingscontinuous-mappingsinclusion-mappingsproofwikitopological-subspaces
Let and be topological spaces. Let . Let be a topological subspace of . Let be the inclusion mapping. Let and be mappings. Then the following apply
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Continuity_of_Composite_with_Inclusion {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] (s : Set α) (f : α → β) (hf : Continuous f) : Continuous (fun x : s => f ↑x) := by sorrySource