const_bind_eq_comp_const — Mathlib

English

The constant kernel composed with a measure equals the composition of the kernel with the constant measure, i.e., const α (μ.bind κ) = κ ∘ₖ const α μ.

Русский

Пусть константное ядро при композиции с мерой эквивалентно композиции ядра с константной мерой: const α (μ.bind κ) = κ ∘ₖ const α μ.

LaTeX

$$$\\mathrm{const}\\, α\\ (\\mu \\bind \\kappa) = \\kappa \\circ_\\\\!\\mathrm{const}\\, α\\ μ$$$

Lean4

@[deprecated comp_const (since := "2025-08-06")]
theorem const_bind_eq_comp_const (κ : Kernel α β) (μ : Measure α) : const α (μ.bind κ) = κ ∘ₖ const α μ :=
  by
  ext a s hs
  simp_rw [comp_apply' _ _ _ hs, const_apply, Measure.bind_apply hs (Kernel.aemeasurable _)]

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