const_inner — Mathlib

English

If φ is integrable, then its image under a continuous linear map is integrable.

Русский

Если φ интегрируемо, то образ под непрерывно линейным отображением интегрируем.

LaTeX

$$$ \\operatorname{Integrable}(\\phi,\\mu) \\Rightarrow \\operatorname{Integrable}(x \\mapsto L(\\phi(x)),\\mu)$$$

Lean4

@[fun_prop]
theorem const_inner (c : E) (hf : Integrable f μ) : Integrable (fun x => ⟪c, f x⟫) μ := by
  rw [← memLp_one_iff_integrable] at hf ⊢; exact hf.const_inner c

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