complete_univ — Mathlib

English

In a complete uniform space, the whole space is a complete subset.

Русский

В полном равномерном пространстве вся пространство является полным подмножеством.

LaTeX

$$$IsComplete(\\mathrm{univ})$$$

Lean4

theorem complete_univ {α : Type u} [UniformSpace α] [CompleteSpace α] : IsComplete (univ : Set α) := fun f hf _ =>
  by
  rcases CompleteSpace.complete hf with ⟨x, hx⟩
  exact ⟨x, mem_univ x, hx⟩

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