isPathConnected_image — Mathlib

English

A homeomorphism preserves path-connectedness of images.

Русский

Гомеоморфизм сохраняет связность по траекториям образов текущей области.

LaTeX

$$$$\text{If } h:X\to Y \text{ is a homeomorphism, then } \operatorname{IsPathConnected}(h''s) \iff \operatorname{IsPathConnected}(s).$$$$

Lean4

/-- If `h : X → Y` is a homeomorphism, `h(s)` is path-connected iff `s` is. -/
@[simp]
theorem isPathConnected_image {s : Set X} (h : X ≃ₜ Y) : IsPathConnected (h '' s) ↔ IsPathConnected s :=
  h.isInducing.isPathConnected_iff.symm

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