preconnectedSpace_of_forall_constant

English

If every Bool-valued function on α that is continuous is constant, then α is PreconnectedSpace.

Русский

Если для любого отображения α → Bool непрерывная функция на всём пространстве является константой, то пространство α является предсвязанным.

LaTeX

$$PreconnectedSpace α$$

Lean4

/-- A `PreconnectedSpace` version of `isPreconnected_of_forall_constant` -/
theorem preconnectedSpace_of_forall_constant (hs : ∀ f : α → Bool, Continuous f → ∀ x y, f x = f y) :
    PreconnectedSpace α :=
  ⟨isPreconnected_of_forall_constant fun f hf x _ y _ => hs f (continuousOn_univ.mp hf) x y⟩

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