comap_zero — Mathlib

English

For any measurable g, the comap of the zero kernel along g is the zero kernel: comap (0 : Kernel α β) g hg = 0.

Русский

Для любого измеримого отображения g нулевое ядро при комапе вдоль g равно нулю: comap (0 : Kernel α β) g hg = 0.

LaTeX

$$$ \operatorname{comap}(0 : \mathrm{Kernel} \ α \ β) \ g hg = 0 $$$

Lean4

@[simp]
theorem comap_zero (hg : Measurable g) : Kernel.comap (0 : Kernel α β) g hg = 0 := by ext; rw [Kernel.comap_apply]; simp

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