connectedSpace — Mathlib

English

If α is connected and f: α → β is surjective and continuous, then β is connected.

Русский

Если α связано, а f: α → β сюръективно и непрерывно, то β связано.

LaTeX

$$$$ConnectedSpace(\\beta)$$$$

Lean4

theorem connectedSpace [ConnectedSpace α] [TopologicalSpace β] {f : α → β} (hf : Surjective f) (hf' : Continuous f) :
    ConnectedSpace β := by
  rw [connectedSpace_iff_univ, ← hf.range_eq]
  exact isConnected_range hf'

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