lintegral_prodMkLeft — Mathlib

English

Let κ be a kernel α → β, ca = (c, a) ∈ γ × α, and g : β → ℝ≥0∞. Then the lower integral of g with respect to prodMkLeft γ κ at ca equals the lower integral of g with respect to κ at ca.snd.

Русский

Пусть κ — ядро α → β, ca = (c, a) ∈ γ × α, и g: β → ℝ≥0∞. Тогда лин.интеграл g по мере prodMkLeft γ κ в ca равен лин.интегралу по κ в ca.snd.

LaTeX

$$$\displaystyle \int^{-} b \, g(b) \\partial prodMkLeft \\gamma \\kappa \\; ca = \int^{-} b \, g(b) \\partial \kappa \\; ca.snd$$$

Lean4

theorem lintegral_prodMkLeft (κ : Kernel α β) (ca : γ × α) (g : β → ℝ≥0∞) :
    ∫⁻ b, g b ∂prodMkLeft γ κ ca = ∫⁻ b, g b ∂κ ca.snd :=
  rfl

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