Continuous_Image_of_Connected_Space_is_Connected
Provedconnectednessproofwikitopology
The continuous image of a connected set is connected.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Continuous_Image_of_Connected_Space_is_Connected {X Y : Type _} [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : Continuous f) (S : Set X) (hS : IsConnected S) : IsConnected (f '' S) := by sorrySource