condExpKernel_apply_eq_condDistrib

English

For nonempty Ω, and any ω, (condExpKernel μ m) ω equals condDistrib id id μ evaluated at id ω.

Русский

Для любого не пустого Ω и любого элемента ω выполняется равенство (condExpKernel μ m) ω = condDistrib id id μ (id ω).

LaTeX

$$$(\\operatorname{condExpKernel} \\mu m)(\\omega) = \\operatorname{condDistrib}(\\mathrm{id},\\mathrm{id},\\mu)(\\mathrm{id}(\\omega))$$$

Lean4

theorem condExpKernel_apply_eq_condDistrib [Nonempty Ω] {ω : Ω} :
    condExpKernel μ m ω = @condDistrib Ω Ω Ω mΩ _ _ mΩ (m ⊓ mΩ) id id μ _ (id ω) := by
  simp [condExpKernel_eq, Kernel.comap_apply]

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