nndist — Mathlib

English

The map p ↦ nndist(p1,p2) is continuous; further, if a function is continuous at every point, the corresponding nndist expression is continuous.

Русский

Отображение p ↦ nndist(p1,p2) непрерывно; далее, если функция непрерывна в каждой точке, соответствующее выражение nndist также непрерывно.

LaTeX

$$$\text{continuous}(\lambda p, \mathrm{nndist}(p_1,p_2))$$$

Lean4

@[fun_prop]
protected theorem nndist [TopologicalSpace β] {f g : β → α} (hf : Continuous f) (hg : Continuous g) :
    Continuous fun b => nndist (f b) (g b) :=
  continuous_nndist.comp₂ hf hg

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