isPreconnected_image — Mathlib

English

Let h be a homeomorphism X ≃ₜ Y. A subset s ⊆ X is preconnected iff its image h[s] ⊆ Y is preconnected.

Русский

Пусть h — гомеоморфизм. Подмножество s ⊆ X является предсоединенным тогда и только тогда, когда его образ h[s] ⊆ Y предсоединен.

LaTeX

$$$IsPreconnected(h(s)) \\iff IsPreconnected(s)$$$

Lean4

@[simp]
theorem isPreconnected_image {s : Set X} (h : X ≃ₜ Y) : IsPreconnected (h '' s) ↔ IsPreconnected s :=
  ⟨fun hs ↦ by simpa only [image_symm, preimage_image] using hs.image _ h.symm.continuous.continuousOn, fun hs ↦
    hs.image _ h.continuous.continuousOn⟩

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