isClosed_range

Mathlib.Topology.Maps.Basic

URI: https://scilib.ai/kg/mathlib#IsClosedMap.isClosed_range

English

The image (range) of a closed map is closed.

Русский

Образ замкнутого отображения — это замкнутое множество.

LaTeX

$$$IsClosedMap f \\to IsClosed (range f)$$$

Lean4

theorem isClosed_range (hf : IsClosedMap f) : IsClosed (range f) :=
  @image_univ _ _ f ▸ hf _ isClosed_univ

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

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

Разделы

Аффилиация

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