measurable_mk — Mathlib

English

With suitable hypotheses (pseudo-metrizable, Borel space), the function hf.mk f is measurable.

Русский

При подходящих условиях функция hf.mk f измерима.

LaTeX

$$$[\\text{PseudoMetrizableSpace } \\beta] \\Rightarrow [\\text{BorelSpace } \\beta] \\Rightarrow Measurable_m(hf.mk f, \\mu)$$$

Lean4

@[fun_prop]
theorem measurable_mk [PseudoMetrizableSpace β] [MeasurableSpace β] [BorelSpace β] (hf : AEStronglyMeasurable[m] f μ) :
    Measurable[m] (hf.mk f) :=
  hf.stronglyMeasurable_mk.measurable

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