unifIntegrable_congr_ae — Mathlib

English

If f_n =ᵐ[μ] g_n for all n, then UnifIntegrable f p μ ↔ UnifIntegrable g p μ.

Русский

Если для всех n выполняется f_n =^{a.e.}_{μ} g_n, то UnifIntegrable f p μ эквивалентно UnifIntegrable g p μ.

LaTeX

$$$\forall n,\ f_n =^{\mathrm{a.e.}} g_n \Rightarrow \text{UnifIntegrable}(f,p,\mu) \iff \text{UnifIntegrable}(g,p,\mu)$$$

Lean4

theorem unifIntegrable_congr_ae {p : ℝ≥0∞} {f g : ι → α → β} (hfg : ∀ n, f n =ᵐ[μ] g n) :
    UnifIntegrable f p μ ↔ UnifIntegrable g p μ :=
  ⟨fun hf => hf.ae_eq hfg, fun hg => hg.ae_eq fun n => (hfg n).symm⟩

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