smul_continuousOn — Mathlib

English

If f is interval-integrable on [a,b], then the function x ↦ c · f(x) is interval-integrable on [a,b] for any constant c.

Русский

Если f интервал-интегрируема на [a,b], то c·f(x) интервал-интегрируема на [a,b] для любого константного c.

LaTeX

$$$\operatorname{IntervalIntegrable}(f,\mu,a,b) \Rightarrow ∀ c, \operatorname{IntervalIntegrable}(x \mapsto c \cdot f(x),\mu,a,b)$$$

Lean4

theorem smul_continuousOn (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.smul_continuousOn_of_subset hg measurableSet_Ioc isCompact_uIcc Ioc_subset_Icc_self

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