constant — Mathlib

English

If α is a PreconnectedSpace and f: α → Y is continuous into a discrete space Y, then f is constant on α.

Русский

Если пространство α предсоединено и отображение f: α → Y непрерывно в дискретное пространство Y, то f константно на всём α.

LaTeX

$$$\forall x,y \in \alpha:\; f(x) = f(y)$$$

Lean4

/-- A `PreconnectedSpace` version of `isPreconnected.constant` -/
theorem constant {Y : Type*} [TopologicalSpace Y] [DiscreteTopology Y] (hp : PreconnectedSpace α) {f : α → Y}
    (hf : Continuous f) {x y : α} : f x = f y :=
  IsPreconnected.constant hp.isPreconnected_univ (Continuous.continuousOn hf) trivial trivial

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