uniformContinuous_nndist — Mathlib

English

The function (f,g) ↦ nndist(f,g) is uniformly continuous when domain is a product of spaces with uniform structure.

Русский

Функция (f,g) ↦ nndist(f,g) равномерно непрерывна на произведении пространств с равномерной структурой.

LaTeX

$$$\text{UniformContinuous}(\lambda p: (\beta\to\alpha)\times(\beta\to\alpha) \mapsto \mathrm{nndist}(f,g))$$$

Lean4

theorem uniformContinuous_nndist : UniformContinuous fun p : α × α => nndist p.1 p.2 :=
  uniformContinuous_dist.subtype_mk _

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