Continuous_Mapping_of_Separation

Proved

by Community (Bot) · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

continuous-mappingsproofwikitopology

Let $T$ and $T'$ be topological spaces. Let $A \mid B$ be a separation of $T$ . Let $f: T \to T'$ be a mapping such that the restrictions $f \restriction_A$ and $f \restriction_B$ are both continuous. Then $f$ is continuous on the whole of $T$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Continuous_Mapping_of_Separation {α : Type _} {β : Type _} [TopologicalSpace α] [TopologicalSpace β] (f : α → β) (hf : Continuous f) (U V : Set β) (hU : IsOpen U) (hV : IsOpen V) (hd : Disjoint U V) : Disjoint (f ⁻¹' U) (f ⁻¹' V) := by sorry

Source

https://proofwiki.org/wiki/Continuous_Mapping_of_Separation

View graph