uniformContinuous_extension — Mathlib

English

If f: α → β is defined and β is complete, then the extension of f is uniformly continuous.

Русский

Если f: α → β определено и β - полное, то продолжение f по дополнению является равномерно непрерывным.

LaTeX

$$$\\mathrm{UniformContinuous}(\\mathrm{Completion.extension}(f))$$$

Lean4

theorem uniformContinuous_extension : UniformContinuous (Completion.extension f) :=
  cPkg.uniformContinuous_extend

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