fst_compProd — Mathlib

English

The first projection of the composition product is the original measure μ: (μ ⊗ₘ κ).fst = μ.

Русский

Первая проекция композиционного произведения равна исходной мере μ.

LaTeX

$$$(μ ⊗ₘ κ).fst = μ$}$$

Lean4

@[simp]
theorem fst_compProd (μ : Measure α) [SFinite μ] (κ : Kernel α β) [IsMarkovKernel κ] : (μ ⊗ₘ κ).fst = μ :=
  by
  ext s
  rw [compProd, Measure.fst, ← Kernel.fst_apply, Kernel.fst_compProd, Kernel.const_apply]

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