English
If f is integrable and all inner products with any vector c have zero integral, then the integral of f is zero.
Русский
Если f интегрируемо и для каждого вектора c все внутренние произведения интегрируются в нуль, то интеграл f равен нулю.
LaTeX
$$$ \\operatorname{Integrable}(f,\\mu) \\rightarrow (\\forall c, \\int x, \\langle c, f(x)\\rangle \\partial\\mu = 0) \\Rightarrow \\int x, f(x)\\partial\\mu = 0$$$
Lean4
theorem _root_.integral_inner {f : α → E} (hf : Integrable f μ) (c : E) : ∫ x, ⟪c, f x⟫ ∂μ = ⟪c, ∫ x, f x ∂μ⟫ :=
((innerSL 𝕜 c).restrictScalars ℝ).integral_comp_comm hf