English
Let α and β be uniform spaces, and let f: α → β be uniformly continuous. If g: hatα → β is uniformly continuous and agrees with f on α via the canonical embedding ι: α → hatα, i.e., f(a) = g(ι(a)) for all a ∈ α, then the extension of f to hatα equals g.
Русский
Пусть α и β — равномерные пространства, f: α → β равномерно непрерывен. Если g: hatα → β равномерно непрерывен и совпадает с f на α через каноническое вложение ι: α → hatα, т.е. ∀ a, f(a) = g(ι(a)), тогда продолжение f до hatα равно g.
LaTeX
$$$ (\forall hf: UniformContinuous\, f) \\to (\forall hg: UniformContinuous\, g) \\to (\forall a:\alpha, f(a) = g(ι(a))) \\to pkg.extend f = g $$$
Lean4
theorem extend_unique (hf : UniformContinuous f) {g : hatα → β} (hg : UniformContinuous g)
(h : ∀ a : α, f a = g (ι a)) : pkg.extend f = g :=
by
apply pkg.funext pkg.continuous_extend hg.continuous
simpa only [pkg.extend_coe hf] using h
