comapRight_apply' — Mathlib

English

For a kernel κ, a measurable embedding f, a point a, and a measurable set t, the comapRight measure equals κ(a) evaluated on the image of t via f.

Русский

Для ядра κ, отображения f с измеримым вложением, точки a и измеримого множества t, мера comapRight равна κ(a) на образе t через f.

LaTeX

$$$\\text{comapRight } κ\, hf\, a\, t = κ(a)(f''t)$$$

Lean4

theorem comapRight_apply' (κ : Kernel α β) (hf : MeasurableEmbedding f) (a : α) {t : Set γ} (ht : MeasurableSet t) :
    comapRight κ hf a t = κ a (f '' t) := by
  rw [comapRight_apply, Measure.comap_apply _ hf.injective (fun s => hf.measurableSet_image.mpr) _ ht]

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