snd_apply' — Mathlib

English

For κ : α → β × γ, a ∈ α, and a measurable s ⊆ γ, snd κ a s = κ a (Prod.snd^{-1}(s)).

Русский

Для κ : α → β × γ, a ∈ α и измеримое множество s ⊆ γ, верно snd κ a s = κ a (Prod.snd^{-1}(s)).

LaTeX

$$$snd κ a\\; s = κ a (\\mathrm{Prod.snd}^{-1}'(s)),$ для измеримого $s$$$

Lean4

theorem snd_apply' (κ : Kernel α (β × γ)) (a : α) {s : Set γ} (hs : MeasurableSet s) :
    snd κ a s = κ a (Prod.snd ⁻¹' s) := by rw [snd_apply, Measure.map_apply measurable_snd hs]

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