aemeasurable — Mathlib

English

If f is AEFinStronglyMeasurable, then f is AEMeasurable.

Русский

Если f является AEFinStronglyMeasurable, то она является AEMeasurable.

LaTeX

$$$\text{AEFinStronglyMeasurable}(f, μ) \Rightarrow \text{AEMeasurable}(f, μ).$$$

Lean4

@[aesop 10% apply (rule_sets := [Measurable])]
protected theorem aemeasurable {β} [Zero β] [MeasurableSpace β] [TopologicalSpace β] [PseudoMetrizableSpace β]
    [BorelSpace β] {f : α → β} (hf : AEFinStronglyMeasurable f μ) : AEMeasurable f μ :=
  ⟨hf.mk f, hf.finStronglyMeasurable_mk.measurable, hf.ae_eq_mk⟩

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