swapRight_apply' — Mathlib

English

For κ, a and a measurable set s ⊆ γ × β, the right-swap measure of s equals the original κ(a) measure of the swapped preimage of s: swapRight κ a (s) = κ a {p | p.swap ∈ s}.

Русский

Для κ, a и измеримого множества s ⊆ γ × β выполняется: swapRight κ a (s) = κ a {p | p.swap ∈ s}.

LaTeX

$$$$swapRight \\kappa a \\; S \;=\\; \\kappa a \\{ p \\mid p.swap \\in S \\} \\quad (S \\subseteq \\gamma \\times \\beta)$$$$

Lean4

theorem swapRight_apply' (κ : Kernel α (β × γ)) (a : α) {s : Set (γ × β)} (hs : MeasurableSet s) :
    swapRight κ a s = κ a {p | p.swap ∈ s} := by rw [swapRight_apply, Measure.map_apply measurable_swap hs]; rfl

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