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⟩