infDist — Mathlib

English

If f: β → α is measurable, then for any fixed s ⊆ α, the function b ↦ infDist(f(b), s) is measurable.

Русский

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

LaTeX

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

Lean4

@[measurability, fun_prop]
theorem infDist {f : β → α} (hf : Measurable f) {s : Set α} : Measurable fun x => infDist (f x) s :=
  measurable_infDist.comp hf

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