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