English
The image of a connected set is connected.
Русский
Образ связного множества является связным.
LaTeX
$$$\\mathrm{IsConnected}(s) \\Rightarrow \\text{ContinuousOn}(f,s) \\Rightarrow \\mathrm{IsConnected}(f''s)$$$
Lean4
/-- The image of a connected set is connected as well. -/
protected theorem image [TopologicalSpace β] {s : Set α} (H : IsConnected s) (f : α → β) (hf : ContinuousOn f s) :
IsConnected (f '' s) :=
⟨image_nonempty.mpr H.nonempty, H.isPreconnected.image f hf⟩