isLindelof_range

Mathlib.Topology.Compactness.Lindelof

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

← MathLib Explorer

English

If X is Lindelöf and f: X→Y is continuous, then the range of f is Lindelöf.

Русский

Если X Линдельфово и f: X→Y непрерывно, то образ f(X) Линдельфов.

LaTeX

$$$[LindelofSpace X]\ {f:X→Y}\ (hf: Continuous f) : IsLindelof (range f)$$$

Lean4

theorem isLindelof_range [LindelofSpace X] {f : X → Y} (hf : Continuous f) : IsLindelof (range f) := by
  rw [← image_univ]; exact isLindelof_univ.image hf

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

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

Разделы

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

Аффилиация

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