smul_of_top_left — Mathlib

English

If f : α → 𝕜 is integrable, then for any c in β, the function x ↦ f(x) • c is integrable.

Русский

Если f: α → 𝕜 интегрируема, то для любого c ∈ β функция x ↦ f(x) • c интегрируема.

LaTeX

$$$\mathrm{Integrable}(f,\mu) \Rightarrow \forall c, \mathrm{Integrable}(x \mapsto f(x) \cdot c, \mu).$$$

Lean4

theorem smul_of_top_left {f : α → β} {φ : α → 𝕜} (hφ : Integrable φ μ) (hf : MemLp f ∞ μ) : Integrable (φ • f) μ :=
  by
  rw [← memLp_one_iff_integrable] at hφ ⊢
  exact MemLp.smul hf hφ

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