integrable_add_iff_integrable_left

English

If f is integrable, then the left-simp form holds: Integrable f μ implies equivalence for g.

Русский

Если f интегрируемо, то слева упрощённая форма сохраняется: интегрируемость f μ влечёт эквивалентность для g.

LaTeX

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

Lean4

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

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