continuousOn_mul — Mathlib

English

If f is LocallyIntegrableOn on s and g is ContinuousOn on s, then the product f·g is LocallyIntegrableOn on s.

Русский

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

LaTeX

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

Lean4

theorem continuousOn_mul [T2Space X] (hg : ContinuousOn g K) (hg' : IntegrableOn g' K μ) (hK : IsCompact K) :
    IntegrableOn (fun x => g x * g' x) K μ :=
  hg'.continuousOn_mul_of_subset hg hK hK.measurableSet Subset.rfl

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