English
If f is integrable, then f + g is integrable iff g is integrable (left/right formulations).
Русский
Если f интегрируемо, то f + g интегрируемо тогда и только тогда, когда g интегрируемо (вправо/влево).
LaTeX
$$$\\mathrm{Integrable}(f, μ) \\Rightarrow (\\mathrm{Integrable}(f+g, μ) \\iff \\mathrm{Integrable}(g, μ))$$$
Lean4
/-- if `f` is integrable, then `f + g` is integrable iff `g` is.
See `integrable_add_iff_integrable_right'` for the same statement with `fun x ↦ f x + g x` instead
of `f + g`. -/
@[simp]
theorem integrable_add_iff_integrable_right {f g : α → β} (hf : Integrable f μ) :
Integrable (f + g) μ ↔ Integrable g μ :=
⟨fun h ↦ show g = f + g + (-f) by simp only [add_neg_cancel_comm] ▸ h.add hf.neg, fun h ↦ hf.add h⟩