integral_eq_zero_of_forall_integral_inner_eq_zero

English

As above, a general statement that if all inner integrals vanish, then the total integral is zero.

Русский

Как выше, если все внутренние интегралы равны нулю, то общий интеграл равен нулю.

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_eq_zero_of_forall_integral_inner_eq_zero (f : α → E) (hf : Integrable f μ)
    (hf_int : ∀ c : E, ∫ x, ⟪c, f x⟫ ∂μ = 0) : ∫ x, f x ∂μ = 0 := by specialize hf_int (∫ x, f x ∂μ);
  rwa [integral_inner hf, inner_self_eq_zero] at hf_int

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