preconnectedSpace — Mathlib

English

If α is preconnected and f: α → β has dense range and is continuous, then β is preconnected.

Русский

Если α предсвязано и f: α → β имеет плотное образ и непрерывен, то β предсвязано.

LaTeX

$$$$PreconnectedSpace(\\beta)$$$$

Lean4

theorem preconnectedSpace [TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (hf : DenseRange f)
    (hc : Continuous f) : PreconnectedSpace β :=
  ⟨hf.closure_eq ▸ (isPreconnected_range hc).closure⟩

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