infEdist — Mathlib

English

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

Русский

Если f: β → α измеримо, то b ↦ infEdist(f(b), s) измеримо.

LaTeX

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

Lean4

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

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