of_forall_diff_eq_zero — Mathlib

English

If f is an Lp function with μ(s) ≠ ∞ and p ≥ 1, then f is integrable on s.

Русский

Если f ∈ Lp и μ(s) ≠ ∞, то f интегрируем на s.

LaTeX

$$IntegrableOn f s μ$$

Lean4

/-- If a function is integrable on a set `s`, and vanishes on `t \ s`, then it is integrable on `t`
if `t` is measurable. -/
theorem of_forall_diff_eq_zero {f : α → ε'} (hf : IntegrableOn f s μ) (ht : MeasurableSet t)
    (h't : ∀ x ∈ t \ s, f x = 0) : IntegrableOn f t μ :=
  hf.of_ae_diff_eq_zero ht.nullMeasurableSet (Eventually.of_forall h't)

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