isPathConnected_preimage — Mathlib

English

If h is a homeomorphism, the preimage of a path-connected set is path-connected iff the set is.

Русский

Если h — гомеоморфизм, то предобраз связной по траекториям множества относительно образа сохраняет/отражает связность по траекториям.

LaTeX

$$$$\text{If } h:X\to Y \text{ is a homeomorphism},\ IsPathConnected(h^{-1}(s)) \iff IsPathConnected(s).$$$$

Lean4

/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is path-connected iff `s` is. -/
@[simp]
theorem isPathConnected_preimage {s : Set Y} (h : X ≃ₜ Y) : IsPathConnected (h ⁻¹' s) ↔ IsPathConnected s := by
  rw [← Homeomorph.image_symm]; exact h.symm.isPathConnected_image

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