comp_discard' — Mathlib

English

Discard after kernel composition with κ equals discard α.

Русский

После композиции ядра с κ следует discard α.

LaTeX

$$$(\\text{discard } β) \\circ \\kappa = \\text{discard } α$$$

Lean4

theorem comp_discard' (κ : Kernel α β) :
    discard β ∘ₖ κ =
      { toFun a := κ a .univ • Measure.dirac ()
        measurable' := (κ.measurable_coe .univ).smul_measure _ } :=
  by
  ext a s hs
  simp [comp_apply' _ _ _ hs, mul_comm]

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