aemeasurable_of_subsingleton_codomain

English

If the codomain is a singleton (subsingleton), any function is AEMeasurable with respect to μ.

Русский

Если кодом значения является одиночное множество, любая функция μ-почти измерима.

LaTeX

$$$\\\\forall f:\\\\alpha \\\\to \\\\beta, \\\\text{AEMeasurable}(f,\\\\mu)$$$

Lean4

@[nontriviality, measurability]
theorem aemeasurable_of_subsingleton_codomain [Subsingleton β] : AEMeasurable f μ :=
  (measurable_of_subsingleton_codomain f).aemeasurable

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