mul_continuousOn — Mathlib

English

If A ⊆ K and K is locally closed, and f ∈ LocallyIntegrableOn on s with ContinuousOn g, then a scaled version is LocallyIntegrableOn on A.

Русский

Если A ⊆ K и K локально замкнуто, и f локально интегрируем на s, а g непрерывна, то масштабированная функция локально интегрируема на A.

LaTeX

$$$\text{LocallyIntegrableOn}(f,g,A,\mu)$$$

Lean4

theorem mul_continuousOn [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 => f x * g x) s μ :=
  by
  rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢
  exact fun k hk_sub hk_c => (hf k hk_sub hk_c).mul_continuousOn (hg.mono hk_sub) hk_c

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