parallelComp_apply_univ — Mathlib

English

For sfinite κ and η, the value of the parallel composition at x on the universal set equals the product of the marginal masses on the universal sets.

Русский

При конечных ядрах κ и η значение на единичном множестве равно произведению масс на единичном множестве для каждой стороны.

LaTeX

$$$$(κ ∥ₖ η) x \\mathrm{univ} = (κ x.1 \\mathrm{univ}) \\cdot (η x.2 \\mathrm{univ}).$$$$

Lean4

@[simp]
theorem parallelComp_apply_univ [IsSFiniteKernel κ] [IsSFiniteKernel η] :
    (κ ∥ₖ η) x Set.univ = κ x.1 Set.univ * η x.2 Set.univ :=
  by
  rw [parallelComp_apply, Measure.prod_apply .univ, mul_comm]
  simp

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