aestronglyMeasurable_congr — Mathlib

English

If f is AEStronglyMeasurable on the trimmed measure μ.trim hm₀, then it is AEStronglyMeasurable on μ.

Русский

Если f AE‑строго измерима по обрезанной мере μtrim, то она AE‑строго измерима по μ.

LaTeX

$$$AEStronglyMeasurable_m(f, μ.trim hm₀) \\Rightarrow AEStronglyMeasurable_m(f, μ)$$$

Lean4

theorem _root_.aestronglyMeasurable_congr (h : f =ᵐ[μ] g) : AEStronglyMeasurable[m] f μ ↔ AEStronglyMeasurable[m] g μ :=
  ⟨fun hf => hf.congr h, fun hg => hg.congr h.symm⟩

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