nndist — Mathlib

English

The function (p) ↦ edist p.1 p.2 from α × α to the extended nonnegative reals is measurable.

Русский

Отображение p ↦ edist(p.1, p.2) из α × α в ℝ≥0∞ измеримо.

LaTeX

$$$\\text{Measurable}(p \\mapsto \\operatorname{edist}(p_1, p_2)).$$$

Lean4

@[measurability, fun_prop]
theorem nndist {f g : β → α} (hf : Measurable f) (hg : Measurable g) : Measurable fun b => nndist (f b) (g b) :=
  (@continuous_nndist α _).measurable2 hf hg

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