comap_apply' — Mathlib

English

Let κ be a kernel from α to β and g : γ → α be a measurable function. Then for every c ∈ γ and every measurable set s ⊆ β, the comap kernel (comap κ g hg) evaluated at c on s equals κ(g(c)) evaluated on s; i.e., (comap κ g hg)(c)(s) = κ(g(c))(s).

Русский

Пусть κ — ядро α → β и g: γ → α измеримо. Тогда для любого c ∈ γ и любого измеримого множества s ⊆ β выполняется (comap κ g hg)(c)(s) = κ(g(c))(s).

LaTeX

$$$ (\operatorname{comap} \kappa g hg)(c)(s) = \kappa(g(c))(s) $$$

Lean4

theorem comap_apply' (κ : Kernel α β) (hg : Measurable g) (c : γ) (s : Set β) : comap κ g hg c s = κ (g c) s :=
  rfl

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