Continuity_from_Union_of_Restrictions
Provedcontinuous-mappingsproofwikitopology
Let and be topological spaces. Then is continuous if either where each is closed in , and the restriction is continuous for each or where is any (possibly infinite) indexing set; each is open in , and the restriction is continuous for each .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Continuity_from_Union_of_Restrictions {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (s t : Set α) (hs : IsClosed s) (ht : IsClosed t) (hst : s ∪ t = Set.univ) (hfs : ContinuousOn f s) (hft : ContinuousOn f t) : Continuous f := by sorrySource