isConnected_range

Mathlib.Topology.Connected.Basic

URI: https://scilib.ai/kg/mathlib#isConnected_range

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

theorem isConnected_range [TopologicalSpace β] [ConnectedSpace α] {f : α → β} (h : Continuous f) :
    IsConnected (range f) :=
  ⟨range_nonempty f, isPreconnected_range h⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru