isProperMap_id

Mathlib.Topology.Maps.Proper.Basic

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

English

A closed embedding is proper.

Русский

Замкнутое вложение проперно.

LaTeX

$$$IsClosedEmbedding(f) \Rightarrow IsProperMap(f)$$$

Lean4

/-- The identity is proper. -/
@[simp]
theorem isProperMap_id : IsProperMap (id : X → X) :=
  IsHomeomorph.id.isProperMap

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

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

Разделы

Аффилиация

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