continuousOn_mul — Mathlib

English

If f is interval-integrable on [a,b] and g is continuous on [a,b], then g·f is interval-integrable on [a,b].

Русский

Если f интервал-интегрируема на [a,b], а g непрерывна на [a,b], то g·f интервал-интегрируема на [a,b].

LaTeX

$$$\operatorname{IntervalIntegrable}(f,\mu,a,b) \Rightarrow \operatorname{ContinuousOn}(g,[a,b]) \Rightarrow \operatorname{IntervalIntegrable}(x \mapsto g(x)\,f(x),\mu,a,b)$$$

Lean4

theorem continuousOn_mul {f g : ℝ → A} (hf : IntervalIntegrable f μ a b) (hg : ContinuousOn g [[a, b]]) :
    IntervalIntegrable (fun x => g x * f x) μ a b :=
  by
  rw [intervalIntegrable_iff] at hf ⊢
  exact hf.continuousOn_mul_of_subset hg isCompact_uIcc measurableSet_Ioc Ioc_subset_Icc_self

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