compProd_id_eq_copy_comp — Mathlib

English

For μ finite and κ a kernel, μ ⊗ₘ κ = (Kernel.id ×ₖ κ) ∘ₘ μ.

Русский

Для конечной μ и ядра κ имеет место равенство μ ⊗ₘ κ = (id × κ) ∘ μ.

LaTeX

$$$[SFinite(\\mu)] [IsSFiniteKernel(κ)] \\\\Rightarrow \\mu \\otimes_{m} \\kappa = (\\text{Kernel.id} \\times_{k} \\kappa) \\circ_{m} \\mu$$$

Lean4

theorem compProd_id_eq_copy_comp [SFinite μ] : μ ⊗ₘ Kernel.id = Kernel.copy α ∘ₘ μ := by
  rw [compProd_id, Kernel.copy, deterministic_comp_eq_map]

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