extension_coe — Mathlib

English

For [T0Space B] and hf uniform continuous, the extension at a equals f a for a in α.

Русский

Для [T0Space B] и равномерно непрерывной f выполняется: $(\\mathrm{extension} f)(a)=f(a)$ для каждого $a\\in \\alpha$.

LaTeX

$$$(\\mathrm{Completion.extension}(f))(a) = f(a)\\quad \\text{for all } a\\in \\alpha$$$

Lean4

theorem extension_coe [T0Space β] (hf : UniformContinuous f) (a : α) : (Completion.extension f) a = f a :=
  cPkg.extend_coe hf a

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