integrable_add_iff_integrable_left'

English

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

Русский

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

LaTeX

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

Lean4

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

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