continuousOn_mul — Mathlib

English

If f is locally integrable on s and g is continuous on s, and s is locally closed, then g f is locally integrable on s.

Русский

Если f локально интегрируемо на s, а g непрерывно на s, и s локально замкнуто, то g f локально интегрируемо на s.

LaTeX

$$LocallyIntegrableOn f s μ → ContinuousOn g s → IsLocallyClosed s → LocallyIntegrableOn (fun x => g x * f x) s μ$$

Lean4

theorem continuousOn_mul [LocallyCompactSpace X] [T2Space X] [NormedRing R] [SecondCountableTopologyEither X R]
    {f g : X → R} {s : Set X} (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) (hs : IsLocallyClosed s) :
    LocallyIntegrableOn (fun x => g x * f x) s μ :=
  by
  rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
  exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_mul (hg.mono hk_sub) hk_c

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