instCompleteSpace

Mathlib.Topology.UniformSpace.Cauchy

URI: https://scilib.ai/kg/mathlib#DiscreteUniformity.instCompleteSpace

← MathLib Explorer

English

CompleteSpace α is equivalent to IsComplete univ.

Русский

Полнота пространства эквивалентна полноте вселенной.

LaTeX

$$$CompleteSpace(\\alpha) \\iff IsComplete(\\mathrm{univ})$$$

Lean4

/-- The discrete uniformity makes a space complete. -/
instance : CompleteSpace α where
  complete {f}
    hf := by
    obtain ⟨x, rfl⟩ := eq_pure_of_cauchy hf
    exact ⟨x, pure_le_nhds x⟩

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

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

Разделы

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

Аффилиация

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