of_discrete — Mathlib

English

If α is countable and has a measurable singleton class, then any f: α → β is AEStronglyMeasurable.

Русский

Если α счетно и имеет множество одиночек измеримого класса, то любая f: α → β аэр AE‑строго измерима.

LaTeX

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

Lean4

@[fun_prop]
theorem of_discrete [Countable α] [MeasurableSingletonClass α] : AEStronglyMeasurable f μ :=
  StronglyMeasurable.of_discrete.aestronglyMeasurable

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