preconnectedSpace — Mathlib

English

If s is preconnected, then the subspace s (with the subspace topology) is preconnected.

Русский

Если множество s предсвязано, то подпространство s с подпространной топологией предсвязано.

LaTeX

$$$$\\text{PreconnectedSpace}(s)$$$$

Lean4

theorem preconnectedSpace {s : Set α} (h : IsPreconnected s) : PreconnectedSpace s where
  isPreconnected_univ := by rwa [← IsInducing.subtypeVal.isPreconnected_image, image_univ, Subtype.range_val]

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