prod_apply_prod — Mathlib

English

For s ⊆ β and t ⊆ γ, (κ.prod η) a (s ×ˢ t) equals (κ a s) · (η a t).

Русский

Для s ⊆ β и t ⊆ γ, (κ.prod η) a (s ×ˢ t) = (κ a s) · (η a t).

LaTeX

$$$$(κ ×ₖ η) a (s ×ˢ t) = (κ a s) \\cdot (η a t).$$$$

Lean4

theorem prod_apply_prod {κ : Kernel α β} {η : Kernel α γ} [IsSFiniteKernel κ] [IsSFiniteKernel η] {s : Set β}
    {t : Set γ} {a : α} : (κ ×ₖ η) a (s ×ˢ t) = (κ a s) * (η a t) := by rw [prod_apply, Measure.prod_prod]

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