not_isMarkovKernel_zero — Mathlib

English

For any measurable set s, the map a ↦ κ(a)(s) is measurable.

Русский

Для любого измеримого множества s отображение a ↦ κ(a)(s) является измеримым.

LaTeX

$$$s\\text{ MeasurableSet} \\Rightarrow \\text{Measurable}(a \\mapsto κ(a)(s))$$$

Lean4

theorem not_isMarkovKernel_zero [Nonempty α] : ¬IsMarkovKernel (0 : Kernel α β) :=
  by
  by_contra h
  let x : α := Nonempty.some inferInstance
  have h1 : (0 : Measure β) .univ = 1 := (h.isProbabilityMeasure x).measure_univ
  simp at h1

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