add — Mathlib

English

If f and g are integrable, then their sum f+g is integrable.

Русский

Если f и g интегрируемы, то их сумма f+g интегрируема.

LaTeX

$$Integrable(f) \rightarrow Integrable(g) \rightarrow Integrable(f+g)$$

Lean4

theorem add {f g : α →ₘ[μ] β} : Integrable f → Integrable g → Integrable (f + g) :=
  by
  refine induction_on₂ f g fun f hf g hg hfi hgi => ?_
  simp only [integrable_mk, mk_add_mk] at hfi hgi ⊢
  exact hfi.add hgi

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