measure_preimage_snd_singleton_eq_tsum

English

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

Русский

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

LaTeX

$$$\mu(\mathrm{Prod.snd} \! ^{-1} \{y\}) = \sum_{x} \mu\{(x,y)\}$, при счётности α.$$

Lean4

theorem measure_preimage_snd_singleton_eq_tsum [Countable α] (μ : Measure (α × β)) (y : β) :
    μ (Prod.snd ⁻¹' { y }) = ∑' x, μ {(x, y)} :=
  by
  have : Prod.snd ⁻¹' { y } = ⋃ x : α, {(x, y)} := by ext y; simp [Prod.ext_iff, eq_comm]
  rw [this, measure_iUnion] <;> simp [Pairwise]

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