mul_continuousOn — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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