compProd_zero_right — Mathlib

English

If κ is S-finite and η is Markov, then (κ ⊗ₖ η) a Set.univ = κ a Set.univ.

Русский

Пусть κ S-ограничено и η марковно; тогда (κ ⊗ₖ η) a Set.univ = κ a Set.univ.

LaTeX

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

Lean4

@[simp]
theorem compProd_zero_right (κ : Kernel α β) (γ : Type*) {mγ : MeasurableSpace γ} : κ ⊗ₖ (0 : Kernel (α × β) γ) = 0 :=
  by
  by_cases h : IsSFiniteKernel κ
  · ext a s hs
    rw [Kernel.compProd_apply hs]
    simp
  · rw [Kernel.compProd_of_not_isSFiniteKernel_left _ _ h]

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