measure_preimage_snd_singleton_eq_sum

English

For a finite α, μ(Prod.snd⁻¹' {y}) = ∑ x μ{(x,y)}.

Русский

Для конечного α верно: μ(прообраз snd от {y}) = сумма по x μ{(x,y)}.

LaTeX

$$$[\text{Fintype }\alpha] \; \Rightarrow \mu(\mathrm{Prod.snd} \! ^{-1} \{y\}) = \sum_{x} \mu\{(x,y)\}.$$$

Lean4

theorem measure_preimage_snd_singleton_eq_sum [Fintype α] (μ : Measure (α × β)) (y : β) :
    μ (Prod.snd ⁻¹' { y }) = ∑ x, μ {(x, y)} := by rw [measure_preimage_snd_singleton_eq_tsum μ y, tsum_fintype]

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