extend_def — Mathlib

English

If f is uniformly continuous, the extension operator agrees with the dense extension on hatα: extend f equals the dense extension of f.

Русский

Если f равномерно непрерывна, то оператор продления согласуется с плотным продолжением: extend f = denseInducing.extend f.

LaTeX

$$$\\text{extend}_def\\ (hf) : pkg.extend f = pkg.isDenseInducing.extend f$$$

Lean4

theorem extend_def (hf : UniformContinuous f) : pkg.extend f = pkg.isDenseInducing.extend f :=
  if_pos hf

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