integrable_add_iff_integrable_right'

English

If f is integrable, then f + g is integrable iff g is integrable (simplified form).

Русский

Если f интегрируемо, то f + g интегрируемо тогда и только тогда, когда g интегрируемо (упрощённая форма).

LaTeX

$$$\\mathrm{Integrable}(f, μ) \\Rightarrow (\\mathrm{Integrable}(f+g, μ) \\iff \\mathrm{Integrable}(g, μ))$$$

Lean4

/-- if `f` is integrable, then `fun x ↦ f x + g x` is integrable iff `g` is.
See `integrable_add_iff_integrable_right` for the same statement with `f + g` instead
of `fun x ↦ f x + g x`. -/
@[simp]
theorem integrable_add_iff_integrable_right' {f g : α → β} (hf : Integrable f μ) :
    Integrable (fun x ↦ f x + g x) μ ↔ Integrable g μ :=
  integrable_add_iff_integrable_right hf

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