uniformContinuous_extend — Mathlib

English

The extension map extend f is uniformly continuous when α is complete and f is continuous, else trivial when not.

Русский

Расширение extend f равномерно непрерывно (при подходящих условиях).

LaTeX

$$$\\forall f:\\alpha\\to\\beta,\\ UniformContinuous(\\mathrm{extend}\\ f)$$$

Lean4

theorem uniformContinuous_extend {f : α → β} : UniformContinuous (extend f) :=
  by
  by_cases hf : UniformContinuous f
  · rw [extend, if_pos hf]
    exact uniformContinuous_uniformly_extend isUniformInducing_pureCauchy denseRange_pureCauchy hf
  · rw [extend, if_neg hf]
    exact uniformContinuous_of_const fun a _b => by congr

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