instCompleteSpace — Mathlib

English

If β is a complete uniform space, then the space of uniformly continuous functions α →ᵤ β (with the uniform convergence topology) is complete.

Русский

Если β — полное пространство с равномерным расстоянием, то пространство равномепрямых функций α →ᵤ β полно.

LaTeX

$$$\\mathrm{CompleteSpace}(\\alpha \\to^{\\mathrm{u}} \\beta)$$$

Lean4

instance {α β : Type*} [UniformSpace β] [CompleteSpace β] : CompleteSpace (α →ᵤ β) :=
  (UniformOnFun.uniformEquivUniformFun β { univ } (mem_singleton _)).completeSpace_iff.1 inferInstance

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