id_prod_apply' — Mathlib

English

For κ : Kernel α β and measurable s, the equality with the prod kernel shows that applying id inside the prod corresponds to preimage under the map a ↦ (a, ·).

Русский

Для κ: Kernel α β и измеримого s равносильно, что применение id внутри произведения эквивалентно предобразованию под отображением a ↦ (a, ·).

LaTeX

$$$\\displaystyle \\big((\\mathrm{Kernel}.id \\times_K \\kappa) a\\big)(s) = \\kappa a (\\mathrm{Prod.mk} a^{-1} s)$$$

Lean4

theorem id_prod_apply' (κ : Kernel α β) [IsSFiniteKernel κ] (a : α) {s : Set (α × β)} (hs : MeasurableSet s) :
    (Kernel.id ×ₖ κ) a s = κ a (Prod.mk a ⁻¹' s) := by rw [Kernel.id, deterministic_prod_apply' _ _ _ hs, id_eq]

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