mapsTo_connectedComponent — Mathlib

English

A continuous map sends a connected component to a connected component.

Русский

Непрерывное отображение отправляет связанную компоненту в связанную компоненту.

LaTeX

$$$\mathrm{MapsTo}(f, \operatorname{connectedComponent}(x), \operatorname{connectedComponent}(f(x)))$$$

Lean4

theorem mapsTo_connectedComponent [TopologicalSpace β] {f : α → β} (h : Continuous f) (a : α) :
    MapsTo f (connectedComponent a) (connectedComponent (f a)) :=
  mapsTo_iff_image_subset.2 <| h.image_connectedComponent_subset a

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