smul — Mathlib

English

If f is interval-integrable on [a,b], then for any scalar r the function r·f is interval-integrable on [a,b].

Русский

Если f интервал-интегрируема на [a,b], то для любого скаляра r функция r·f тоже интервал-интегрируема на [a,b].

LaTeX

$$$\operatorname{IntervalIntegrable}(f,\mu,a,b) \Rightarrow \forall r, \operatorname{IntervalIntegrable}(r\cdot f,\mu,a,b)$$$

Lean4

theorem smul {R : Type*} [NormedAddCommGroup R] [SMulZeroClass R E] [IsBoundedSMul R E] {f : ℝ → E}
    (h : IntervalIntegrable f μ a b) (r : R) : IntervalIntegrable (r • f) μ a b :=
  ⟨h.1.smul r, h.2.smul r⟩

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