English
A preconnected set s has the property that any map from α to a discrete space Y, which is continuous on s, is constant on s.
Русский
Любое отображение из α в дискретное пространство Y, непрерывное на префиксной части s, константно на s.
LaTeX
$$$\forall x,y \in s:\; f(x) = f(y)$$$
Lean4
/-- A preconnected set `s` has the property that every map to a
discrete space that is continuous on `s` is constant on `s` -/
theorem constant {Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y] {s : Set α} (hs : IsPreconnected s) {f : α → Y}
(hf : ContinuousOn f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) : f x = f y :=
(hs.image f hf).subsingleton (mem_image_of_mem f hx) (mem_image_of_mem f hy)