image_connectedComponent_eq_singleton

English

The image of a connected component under a continuous map into a totally disconnected space is a singleton.

Русский

Образ связанной компоненты под непрерывным отображением в полностью раздельное пространство является синглетоном.

LaTeX

$$$\text{f '' connectedComponent a} = {f a}$$$

Lean4

/-- The image of a connected component in a totally disconnected space is a singleton. -/
@[simp]
theorem image_connectedComponent_eq_singleton {β : Type*} [TopologicalSpace β] [TotallyDisconnectedSpace β] {f : α → β}
    (h : Continuous f) (a : α) : f '' connectedComponent a = {f a} :=
  (Set.subsingleton_iff_singleton <| mem_image_of_mem f mem_connectedComponent).mp
    (isPreconnected_connectedComponent.image f h.continuousOn).subsingleton

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