measurable_nndist — Mathlib

English

If f, g: β → α are measurable, then the function b ↦ nndist(f(b), g(b)) is measurable.

Русский

Если f, g: β → α измеримы, тогда b ↦ nndist(f(b), g(b)) измерима.

LaTeX

$$$\\text{Measurable}(f) \\rightarrow \\text{Measurable}(g) \\rightarrow \\text{Measurable}(b \\mapsto \\mathrm{nndist}(f(b), g(b))).$$$

Lean4

@[measurability]
theorem measurable_nndist : Measurable fun p : α × α => nndist p.1 p.2 :=
  continuous_nndist.measurable

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