const_mul — Mathlib

English

If f is interval-integrable on [a,b] and g is a continuous function taking values in a semiring, then f·g is interval-integrable on [a,b].

Русский

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

LaTeX

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

Lean4

@[simp]
theorem const_mul {f : ℝ → A} (hf : IntervalIntegrable f μ a b) (c : A) : IntervalIntegrable (fun x => c * f x) μ a b :=
  hf.continuousOn_mul continuousOn_const

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