mapsTo_connectedComponentIn — Mathlib

English

A continuous map maps connectedComponentIn s a into connectedComponentIn (f'' s) (f a).

Русский

Непрерывное отображение отображает connectedComponentIn s a в connectedComponentIn (f'' s) (f a).

LaTeX

$$$\mathrm{MapsTo}(f, connectedComponentIn s a, connectedComponentIn (f'' s) (f a))$$$

Lean4

theorem mapsTo_connectedComponentIn [TopologicalSpace β] {f : α → β} {s : Set α} (h : Continuous f) {a : α}
    (hx : a ∈ s) : MapsTo f (connectedComponentIn s a) (connectedComponentIn (f '' s) (f a)) :=
  mapsTo_iff_image_subset.2 <| image_connectedComponentIn_subset h hx

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