stronglyMeasurable — Mathlib

English

A finitely strongly measurable function is measurable (with standard regularity assumptions).

Русский

Функция, финитно сильно измеримая, является измеримой.

LaTeX

$$$\text{FinStronglyMeasurable}(f,\mu) \Rightarrow \text{Measurable}(f)$$$

Lean4

/-- A finitely strongly measurable function is strongly measurable. -/
@[aesop 5% apply (rule_sets := [Measurable])]
protected theorem stronglyMeasurable [Zero β] [TopologicalSpace β] (hf : FinStronglyMeasurable f μ) :
    StronglyMeasurable f :=
  ⟨hf.approx, hf.tendsto_approx⟩

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