integrableOn_isCompact — Mathlib

English

If hf is locally integrable on s and t ⊆ s is compact, then f is integrable on t.

Русский

Если f локально интегрируемо на s и t ⊆ s компактно, то f интегрируема на t.

LaTeX

$$$\\forall t\\subset s, IsCompact(t) \\Rightarrow \\text{IntegrableOn}(f,t,μ)$$$

Lean4

/-- If a function is locally integrable on a compact set, then it is integrable on that set. -/
theorem integrableOn_isCompact [PseudoMetrizableSpace ε] (hf : LocallyIntegrableOn f s μ) (hs : IsCompact s) :
    IntegrableOn f s μ :=
  IsCompact.induction_on hs integrableOn_empty (fun _u _v huv hv => hv.mono_set huv)
    (fun _u _v hu hv => integrableOn_union.mpr ⟨hu, hv⟩) hf

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