measurable_infNndist — Mathlib

English

For f: β → α measurable, the function b ↦ infNndist(f(b), s) is measurable for any fixed s.

Русский

Для измеримого f: β → α функция b ↦ infNndist(f(b), s) измерима для любого фиксированного s.

LaTeX

$$$\\text{Measurable}(f) \\Rightarrow \\forall s,\\ \\text{Measurable}(b \\mapsto \\operatorname{infNndist}(f(b), s)).$$$

Lean4

@[measurability]
theorem measurable_infNndist {s : Set α} : Measurable fun x => infNndist x s :=
  (continuous_infNndist_pt s).measurable

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