inseparable_extension_coe — Mathlib

English

For hf uniform continuous, each extension point is inseparable from its original value: inseparable from f x.

Русский

Для равномерно непрерывной функции hf каждая точка расширения неразделима от своего исходного значения.

LaTeX

$$$\\mathrm{Inseparable}(\\mathrm{Completion.extension}(f)(\\mathrm{coe}'x), f(x))$$$

Lean4

theorem inseparable_extension_coe (hf : UniformContinuous f) (x : α) : Inseparable (Completion.extension f x) (f x) :=
  cPkg.inseparable_extend_coe hf x

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