integrable_add_iff_integrable_right

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⟩

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