withDensity_of_not_measurable — Mathlib

English

If f is not measurable (as a function of two variables), then withDensity κ f is the zero kernel.

Русский

Если f не измеримая функция двух переменных, то withDensity κ f совпадает с нулевым ядром.

LaTeX

$$withDensity κ f = 0$$

Lean4

theorem withDensity_of_not_measurable (κ : Kernel α β) [IsSFiniteKernel κ] (hf : ¬Measurable (Function.uncurry f)) :
    withDensity κ f = 0 := by classical exact dif_neg hf

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