isPreconnected_preimage — Mathlib

English

If h is a homeomorphism, a subset s ⊆ Y is preconnected iff its preimage h^{-1}(s) ⊆ X is preconnected.

Русский

Если h — гомеоморфизм, множество s ⊆ Y является предсоединенным тогда и только тогда, когда его предобраз под h, h^{-1}(s) ⊆ X, предсоединен.

LaTeX

$$$IsPreconnected(h^{-1}(s)) \\iff IsPreconnected(s)$$$

Lean4

@[simp]
theorem isPreconnected_preimage {s : Set Y} (h : X ≃ₜ Y) : IsPreconnected (h ⁻¹' s) ↔ IsPreconnected s := by
  rw [← image_symm, isPreconnected_image]

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