add — Mathlib

English

If f and g are interval-integrable on [a,b], then their sum is interval-integrable on [a,b].

Русский

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

LaTeX

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

Lean4

@[simp]
theorem add [ContinuousAdd ε] (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
    IntervalIntegrable (fun x => f x + g x) μ a b :=
  ⟨hf.1.add hg.1, hf.2.add hg.2⟩

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