dist — Mathlib

English

If f,g are uniformly continuous functions from β to α, then the map b ↦ dist(f(b), g(b)) is uniformly continuous.

Русский

Если f,g — равномерно непрерывные отображения β→α, то b↦dist(f(b), g(b)) равномерно непрерывно.

LaTeX

$$$\forall f,g:β\to α\, (hf: UniformContinuous f) (hg: UniformContinuous g),\ UniformContinuous(\lambda b, dist(f(b),g(b)))$$$

Lean4

protected theorem dist [UniformSpace β] {f g : β → α} (hf : UniformContinuous f) (hg : UniformContinuous g) :
    UniformContinuous fun b => dist (f b) (g b) :=
  uniformContinuous_dist.comp (hf.prodMk hg)

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