isClosed_range

Mathlib.Topology.Maps.Proper.Basic

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

English

The range of a proper map is closed.

Русский

Область проперного отображения замкнута.

LaTeX

$$$IsProperMap(f) \Rightarrow IsClosed(range(f))$$$

Lean4

/-- The range of a proper map is closed. -/
theorem isClosed_range (hf : IsProperMap f) : IsClosed (range f) :=
  hf.isClosedMap.isClosed_range

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

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

Разделы

Аффилиация

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