uniformContinuous_extend — Mathlib

English

The extended map pkg.extend f is continuous (assuming appropriate hypotheses).

Русский

Расширенная карта pkg.extend f непрерывна (при надлежащих предпосылках).

LaTeX

$$$\\text{Continuous}(pkg.extend f)$$$

Lean4

theorem uniformContinuous_extend : UniformContinuous (pkg.extend f) :=
  by
  by_cases hf : UniformContinuous f
  · rw [pkg.extend_def hf]
    exact uniformContinuous_uniformly_extend pkg.isUniformInducing pkg.dense hf
  · unfold AbstractCompletion.extend
    rw [if_neg hf]
    exact uniformContinuous_of_const fun a b => by congr 1

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