lintegral_prodMkRight — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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