image — Mathlib

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⟩

Похожие утверждения