compProd_of_not_isSFiniteKernel — Mathlib

English

Let κ be a kernel that is not S-finite and μ be any measure. Then the composition product μ ⊗ₘ κ is the zero measure.

Русский

Пусть κ — ядро, не являющееся S-финитным; пусть μ — любая мера. Тогда композиционный продукт μ ⊗ₘ κ равен нулевой мере.

LaTeX

$$$\\forall {\\alpha} {\\beta}, \\forall (μ : \\mathrm{Measure}\\; \\alpha), (κ : \\text{Kernel } \\alpha \\beta), (\\neg \\mathrm{IsSFiniteKernel}(κ)) \\implies μ \\otimes_m κ = 0$$$

Lean4

@[simp]
theorem compProd_of_not_isSFiniteKernel (μ : Measure α) (κ : Kernel α β) (h : ¬IsSFiniteKernel κ) : μ ⊗ₘ κ = 0 :=
  by
  rw [compProd, Kernel.compProd_of_not_isSFiniteKernel_right, Kernel.zero_apply]
  rwa [Kernel.isSFiniteKernel_prodMkLeft_unit]

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