comp_const_apply_eq_bind — Mathlib

English

If κ is invariant with respect to μ, then κ ∘ₖ const α μ = const α μ.

Русский

Если κ инвариантно относительно μ, тогда κ ∘ₖ const α μ = const α μ.

LaTeX

$$$\\kappa\\;\\mathrm{Invariant}\\; \\mu \\rightarrow \\kappa \\circ_\\\\!\\mathrm{const}\\, α μ = \\mathrm{const}\\, α μ$$$

Lean4

@[deprecated comp_const (since := "2025-08-06")]
theorem comp_const_apply_eq_bind (κ : Kernel α β) (μ : Measure α) (a : α) : (κ ∘ₖ const α μ) a = μ.bind κ := by
  rw [← const_apply (μ.bind κ) a, comp_const κ μ]

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