isConnected_image — Mathlib

English

If h is a homeomorphism X ≃ₜ Y, then IsConnected(h[s]) holds iff IsConnected(s) for any s ⊆ X (with the image also nonempty).

Русский

Если h — гомеоморфизм X ≃ₜ Y, то множество h[s] соединено тогда и только тогда, когда s соединено (при условии, что образ непуст).

LaTeX

$$$IsConnected(h(s)) \\iff IsConnected(s)$$$

Lean4

@[simp]
theorem isConnected_image {s : Set X} (h : X ≃ₜ Y) : IsConnected (h '' s) ↔ IsConnected s :=
  image_nonempty.and h.isPreconnected_image

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