integral_integral_sub'_comp — Mathlib

English

Analogous lintegral version with subtraction inside the inner integral.

Русский

Линейный интеграл аналогично, с вычитанием внутри вложенного интеграла.

LaTeX

$$$$ \\int^{-}_{x} F\\left(\\int y\\,(f(y) - g(y))\\,d\\eta_x(y)\\right)\\,d\\kappa a = \\int^{-}_{x} F\\left(\\int y\\,f(y)\\,d\\eta_x(y) - \\int y\\,g(y)\\,d\\eta_x(y)\\right)\\,d\\kappa a $$$$

Lean4

theorem integral_integral_sub'_comp ⦃f g : γ → E⦄ (hf : Integrable f ((η ∘ₖ κ) a)) (hg : Integrable g ((η ∘ₖ κ) a)) :
    ∫ x, ∫ y, (f - g) y ∂η x ∂κ a = ∫ x, ∫ y, f y ∂η x ∂κ a - ∫ x, ∫ y, g y ∂η x ∂κ a :=
  integral_integral_sub_comp hf hg

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