pathConnectedSpace — Mathlib

English

If X is path-connected and f: X → Y is surjective and continuous, then Y is path-connected (as a PathConnectedSpace).

Русский

Если X путево связано и f сюръективно и непрерывно отображает X в Y, то Y путево связано.

LaTeX

$$PathConnectedSpace Y$$

Lean4

theorem pathConnectedSpace [PathConnectedSpace X] {f : X → Y} (hf : Surjective f) (hf' : Continuous f) :
    PathConnectedSpace Y := by
  rw [pathConnectedSpace_iff_univ, ← hf.range_eq]
  exact isPathConnected_range hf'

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