image_connectedComponentIn_subset

English

The image of a connectedComponentIn s a is contained in the connectedComponentIn of the image of s at a.

Русский

Образ connectedComponentIn s a содержится в connectedComponentIn (image of s) (a).

LaTeX

$$$f'' connectedComponentIn s a \subseteq connectedComponentIn (f'' s) (f a)$$$

Lean4

theorem image_connectedComponentIn_subset [TopologicalSpace β] {f : α → β} {s : Set α} {a : α} (hf : Continuous f)
    (hx : a ∈ s) : f '' connectedComponentIn s a ⊆ connectedComponentIn (f '' s) (f a) :=
  (isPreconnected_connectedComponentIn.image _ hf.continuousOn).subset_connectedComponentIn
    (mem_image_of_mem _ <| mem_connectedComponentIn hx) (image_mono <| connectedComponentIn_subset _ _)

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