prod_apply' — Mathlib

English

Given κ and η s-finite on α with β and α with γ, for a ∈ α, (κ.prod η) a equals the product of κ a and η a.

Русский

Для произвольного a∈α, (κ.prod η) a = (κ a) ⋅ (η a).

LaTeX

$$$$(κ.prod η) a = (κ a) \\text{.prod} (η a).$$$$

Lean4

theorem prod_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (η : Kernel α γ) [IsSFiniteKernel η] (a : α) {s : Set (β × γ)}
    (hs : MeasurableSet s) : (κ ×ₖ η) a s = ∫⁻ b : β, (η a) (Prod.mk b ⁻¹' s) ∂κ a := by
  simp_rw [prod, comp_apply, copy_apply, Measure.dirac_bind (Kernel.measurable _) (a, a), parallelComp_apply,
    Measure.prod_apply hs]

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