preconnectedSpace — Mathlib

English

If α is Preconnected, then β is Preconnected as well under a dense inducing i.

Русский

Если α — предсоединённое пространство, то и β — предсоединённое пространство (при плотном индуцирующем отображении i).

LaTeX

$$$ [\\text{PreconnectedSpace } α] \\Rightarrow [\\text{PreconnectedSpace } β] \\text{ for dense inducing } i $$$

Lean4

protected theorem preconnectedSpace [PreconnectedSpace α] (di : IsDenseInducing i) : PreconnectedSpace β :=
  di.dense.preconnectedSpace di.continuous

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