of_finite — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[deprecated of_discrete (since := "2025-04-09")]
theorem of_finite [DiscreteMeasurableSpace α] [Finite α] : AEStronglyMeasurable f μ :=
  .of_discrete

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