nndist — Mathlib

English

If f and g are uniformly continuous, then b ↦ nndist(f(b), g(b)) is uniformly continuous.

Русский

Если f и g равномерно непрерывны, то b ↦ nndist(f(b), g(b)) также равномерно непрерывно.

LaTeX

$$$\text{UniformContinuous}(f) \to \text{UniformContinuous}(g) \Rightarrow \text{UniformContinuous}(\lambda b, \mathrm{nndist}(f(b), g(b)))$$$

Lean4

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

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