compProd_apply_univ — Mathlib

English

If κ is a finite S kernel and η is a Markov kernel, then (κ ⊗ₖ η) a of the universal set equals κ a universal set.

Русский

Пусть κ является конечным S-ядром, а η – марковым ядром; тогда (κ ⊗ₖ η) a (универсальное множество) равно κ a (универсальное множество).

LaTeX

$$$$ (κ \otimes_k η) a (\mathsf{Set.univ}) = κ a (\mathsf{Set.univ}). $$$$

Lean4

@[simp]
theorem compProd_apply_univ {κ : Kernel α β} {η : Kernel (α × β) γ} [IsSFiniteKernel κ] [IsMarkovKernel η] {a : α} :
    (κ ⊗ₖ η) a Set.univ = κ a Set.univ :=
  by
  rw [compProd_apply MeasurableSet.univ]
  simp

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