of_inter_support — Mathlib

English

If a function is integrable on s and vanishes on t\s, then integrable on t (when t is measurable).

Русский

Если функция интегрируема на s и обращается в нуль на t\s, то она интегрируема на t при условии, что t измеримо.

LaTeX

$$IntegrableOn f s μ → (∀ x ∈ t\s, f x = 0) → IntegrableOn f t μ$$

Lean4

theorem of_inter_support {f : α → ε'} (hs : MeasurableSet s) (hf : IntegrableOn f (s ∩ support f) μ) :
    IntegrableOn f s μ := by simpa using hf.of_forall_diff_eq_zero hs

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