aestronglyMeasurable' — Mathlib

English

If α is a subsingleton, then any f: α → β is AEStronglyMeasurable with respect to μ.

Русский

Если область определения α — подсубмножество, то любая функция f: α → β является AEStronglyMeasurable по μ.

LaTeX

$$$[\\text{Subsingleton}(\\alpha)] \\Rightarrow AEStronglyMeasurable_m(f, \\mu)$$$

Lean4

@[deprecated AEStronglyMeasurable.of_subsingleton_dom (since := "2025-04-09")]
theorem aestronglyMeasurable' [Subsingleton α] (f : α → β) : AEStronglyMeasurable f μ :=
  .of_subsingleton_dom

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