integrableOn_iff_integrable_of_support_subset

English

If the support of f is contained in s, then integrability on s is equivalent to integrability on entire space.

Русский

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

LaTeX

$$support f ⊆ s → IntegrableOn f s μ ↔ Integrable f μ$$

Lean4

theorem integrableOn_iff_integrable_of_support_subset {f : α → ε'} (h1s : support f ⊆ s) :
    IntegrableOn f s μ ↔ Integrable f μ :=
  by
  refine ⟨fun h => ?_, fun h => h.integrableOn⟩
  refine h.integrable_of_forall_notMem_eq_zero fun x hx => ?_
  contrapose! hx
  exact h1s (mem_support.2 hx)

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