English
Let f: α → β be uniformly continuous and let g: Completion α → β be uniformly continuous. If for every a ∈ α we have f(a) = g(â) where â denotes the canonical embedding of α into Completion α, then the extension of f to Completion α is equal to g; i.e., Completion.extension f = g.
Русский
Пусть f: α → β непрерывно по униформизму и g: Completion α → β непрерывно. Если для каждого a ∈ α выполняется f(a) = g(â), где â является каноническим вложением α в Completion α, то продолжение f до Completion α совпадает с g; то есть Completion.extension f = g.
LaTeX
$$$\\forall f: \\alpha \\to \\beta\\,\\forall g: \\mathrm{Completion}(\\alpha) \\to \\beta\\,\\big(\\mathrm{UniformContinuous} f \\to \\mathrm{UniformContinuous} g \\to (\\forall a:\\alpha, f(a)=g(\\hat a)) \\Rightarrow \\mathrm{Completion.extension} f = g\\big)$$$
Lean4
theorem extension_unique (hf : UniformContinuous f) {g : Completion α → β} (hg : UniformContinuous g)
(h : ∀ a : α, f a = g (a : Completion α)) : Completion.extension f = g :=
cPkg.extend_unique hf hg h
