enorm — Mathlib

English

If hf is locally integrable and g is AEStronglyMeasurable with ‖g‖ ≤ ‖f‖ a.e., then g is locally integrable.

Русский

Если hf локально интегрируемо, а g AE‑сильно измеримо и ‖g‖ ≤ ‖f‖ почти всюду, то g локально интегрируемо.

LaTeX

$$$\\text{LocallyIntegrableOn}(f,s,μ) \\Rightarrow \\text{LocallyIntegrableOn}(g,s,μ)\\quad(‖g‖ ≤ ‖f‖ \\text{ a.e.})$$$

Lean4

theorem enorm (hf : LocallyIntegrableOn f s μ) : LocallyIntegrableOn (‖f ·‖ₑ) s μ := fun t ht ↦
  let ⟨U, hU_nhd, hU_int⟩ := hf t ht
  ⟨U, hU_nhd, hU_int.enorm⟩

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