constant — Mathlib

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)

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