measure_preimage_fst_singleton_eq_tsum

English

For countable β, μ(Prod.fst⁻¹' {x}) equals the sum over β of μ{(x,y)}.

Русский

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

LaTeX

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

Lean4

theorem measure_preimage_fst_singleton_eq_tsum [Countable β] (μ : Measure (α × β)) (x : α) :
    μ (Prod.fst ⁻¹' { x }) = ∑' y, μ {(x, y)} := by
  rw [← measure_iUnion (by simp [Pairwise]) fun _ ↦ .singleton _, iUnion_singleton_eq_range,
    preimage_fst_singleton_eq_range]

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