dirac_unit_compProd — Mathlib

English

The composition of the Dirac measure at unit with κ equals the pushforward by Prod.mk Unit.unit of κ’s value at unit.

Русский

Композиция Dirac на единице и κ равна отображению по Prod.mk Unit.unit от κ(Unit.unit).

LaTeX

$$$\\mathrm{dirac} (\\text{Unit}) ⊗_m κ = (κ (\\text{Unit})).map (\\mathrm{Prod.mk} ())$$$

Lean4

theorem dirac_unit_compProd (κ : Kernel Unit β) [IsSFiniteKernel κ] : Measure.dirac () ⊗ₘ κ = (κ ()).map (Prod.mk ()) :=
  by ext s hs; rw [dirac_compProd_apply hs, Measure.map_apply measurable_prodMk_left hs]

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