complete_of_compact

Mathlib.Topology.UniformSpace.Cauchy

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

← MathLib Explorer

English

A compact space is complete.

Русский

Компактное пространство полно.

LaTeX

$$$$\\text{CompleteSpace}(\\alpha) \\text{ holds if } [CompactSpace(\\alpha)].$$$$

Lean4

instance (priority := 100) complete_of_compact {α : Type u} [UniformSpace α] [CompactSpace α] : CompleteSpace α :=
  ⟨fun hf => by simpa using (isCompact_iff_totallyBounded_isComplete.1 isCompact_univ).2 _ hf⟩

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

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

Разделы

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

Аффилиация

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