aemeasurable — Mathlib

English

If the domain is a singleton (subsingleton), every function is almost everywhere measurable with respect to μ.

Русский

Если область является одноэлементной (subsingleton), любая функция является μ-почти измеримой.

LaTeX

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

Lean4

@[nontriviality, measurability]
theorem aemeasurable [Subsingleton α] : AEMeasurable f μ :=
  Subsingleton.measurable.aemeasurable

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