uniformContinuous_extension₂ — Mathlib

English

The two-argument extension is uniformly continuous: UniformContinuous₂ (Completion.extension₂ f).

Русский

Двухарная функция-расширение равномерно непрерывна: UniformContinuous₂ (Completion.extension₂ f).

LaTeX

$$$\\mathrm{UniformContinuous_2} (\\mathrm{Completion.extension_2} f)$$$

Lean4

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

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