proper_of_compact

Mathlib.Topology.MetricSpace.ProperSpace

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

← MathLib Explorer

English

If a pseudo metric space is compact, then it is proper.

Русский

Если псевдометрическое пространство компактно, то оно правильное.

LaTeX

$$$[CompactSpace\;\alpha] \Rightarrow [ProperSpace\;\alpha]$$$

Lean4

instance (priority := 100) proper_of_compact [CompactSpace α] : ProperSpace α :=
  ⟨fun _ _ => isClosed_closedBall.isCompact⟩
    -- see Note [lower instance priority]

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

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

Разделы

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

Аффилиация

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