aefinStronglyMeasurable — Mathlib

English

The zero function is AEFinStronglyMeasurable for any measure μ when the target space has a zero element.

Русский

Нулевая функция является AEFinStronglyMeasurable для любой меры μ, если простанство имеет нулевой элемент.

LaTeX

$$$ (\\text{Zero}\\ β) \\Rightarrow (\\text{AEFinStronglyMeasurable}\\ (0: α\\rightarrow β)\\ μ) $$$

Lean4

theorem aefinStronglyMeasurable [Zero β] [TopologicalSpace β] (hf : FinStronglyMeasurable f μ) :
    AEFinStronglyMeasurable f μ :=
  ⟨f, hf, ae_eq_refl f⟩

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