image_connectedComponent_subset — Mathlib

English

The image of a connected component under a continuous map is contained in the connected component of the image.

Русский

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

LaTeX

$$$f'' connectedComponent a \subseteq connectedComponent (f a)$$$

Lean4

theorem image_connectedComponent_subset [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) :
    f '' connectedComponent a ⊆ connectedComponent (f a) :=
  (isConnected_connectedComponent.image f h.continuousOn).subset_connectedComponent
    ((mem_image f (connectedComponent a) (f a)).2 ⟨a, mem_connectedComponent, rfl⟩)

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