eq_of_continuous — Mathlib

English

If a continuous map f is defined on a space X that is Preconnected and the codomain is totally disconnected, then f is constant.

Русский

Если непрерывное отображение f определено на предсвязном пространстве X и далее в TD-пространство, то f константно.

LaTeX

$$$\forall i, j:\, f(i) = f(j)$$$

Lean4

theorem eq_of_continuous [TopologicalSpace β] [PreconnectedSpace α] [TotallyDisconnectedSpace β] (f : α → β)
    (hf : Continuous f) (i j : α) : f i = f j :=
  (isPreconnected_univ.image f hf.continuousOn).subsingleton ⟨i, trivial, rfl⟩ ⟨j, trivial, rfl⟩

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