comp_boolKernel — Mathlib

English

κ.comp (boolKernel μ ν) = boolKernel (κ ∘ₘ μ) (κ ∘ₘ ν).

Русский

κ.comp (boolKernel μ ν) = boolKernel (κ ∘ μ) (κ ∘ ν).

LaTeX

$$$\\kappa.comp(\\text{boolKernel }\\mu \\nu) = \\text{boolKernel}(\\mu \\bind \\kappa, \\nu \\bind \\kappa)$$$

Lean4

@[simp]
theorem comp_boolKernel (κ : Kernel α β) (μ ν : Measure α) : κ ∘ₖ (boolKernel μ ν) = boolKernel (κ ∘ₘ μ) (κ ∘ₘ ν) :=
  by
  ext b : 1
  rw [comp_apply]
  cases b <;> simp

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