integrable_of_forall_notMem_eq_zero

English

If a function is integrable on s and vanishes almost everywhere on its complement, then it is integrable on the whole space.

Русский

Если функция интегрируема на s и почти нигде не отлична от нуля на дополнении, то она интегрируема на все пространство.

LaTeX

$$IntegrableOn f s μ → NullMeasurableSet t μ → (ae μ)(x ∈ t\s → f x = 0) → IntegrableOn f t μ$$

Lean4

/-- If a function is integrable on a set `s` and vanishes everywhere on its complement,
then it is integrable. -/
theorem integrable_of_forall_notMem_eq_zero {f : α → ε'} (hf : IntegrableOn f s μ) (h't : ∀ x, x ∉ s → f x = 0) :
    Integrable f μ :=
  hf.integrable_of_ae_notMem_eq_zero (Eventually.of_forall fun x hx => h't x hx)

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