English
Let μ be a finite measure on α and κ, η be finite kernels α → β. Then μ ⊗ₘ κ = μ ⊗ₘ η if and only if κ =ᵐ[μ] η (κ and η are μ-almost everywhere equal).
Русский
Пусть μ — конечная мера на α, а κ, η — конечные ядра α → β. Тогда μ ⊗ₘ κ = μ ⊗ₘ η тогда и только тогда, когда κ =μ-эквивалентно η (они равны μ-почти в смысле).
LaTeX
$$$\\bigl(\\text{IsFiniteMeasure }\\mu\\bigr) \\land \\bigl(\\text{IsFiniteKernel }\\kappa\\bigr) \\land \\bigl(\\text{IsFiniteKernel }\\eta\\bigr) \\Rightarrow \\bigl(\\mu \\otimes_m \\kappa = \\mu \\otimes_m \\eta \\iff \\kappa =^{\\mu} \\eta\\bigr).$$$
Lean4
/-- Two finite kernels `κ` and `η` are `μ`-a.e. equal iff the composition-products `μ ⊗ₘ κ`
and `μ ⊗ₘ η` are equal. -/
theorem compProd_eq_iff [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] : μ ⊗ₘ κ = μ ⊗ₘ η ↔ κ =ᵐ[μ] η :=
⟨Kernel.ae_eq_of_compProd_eq, Measure.compProd_congr⟩
