isPreconnected_range — Mathlib

English

If α is preconnected and f: α → β is continuous, then the image range(f) is preconnected.

Русский

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

LaTeX

$$$$IsPreconnected(\\mathrm{range}(f))$$$$

Lean4

theorem isPreconnected_range [TopologicalSpace β] [PreconnectedSpace α] {f : α → β} (h : Continuous f) :
    IsPreconnected (range f) :=
  @image_univ _ _ f ▸ isPreconnected_univ.image _ h.continuousOn

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