theorem MeasureTheory.measure_preimage_fst_singleton_eq_sum_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] [Countable β] (μ : MeasureTheory.Measure (α × β)) (x : α) : μ (Prod.fst ⁻¹' {x}) = ∑' (y : β), μ {(x, y)}

theorem MeasureTheory.measure_preimage_snd_singleton_eq_sum_countable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] [Countable α] (μ : MeasureTheory.Measure (α × β)) (y : β) : μ (Prod.snd ⁻¹' {y}) = ∑' (x : α), μ {(x, y)}

theorem MeasureTheory.measure_preimage_fst_singleton_eq_sum {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype β] (μ : MeasureTheory.Measure (α × β)) (x : α) : μ (Prod.fst ⁻¹' {x}) = Finset.univ.sum fun (y : β) => μ {(x, y)}

theorem MeasureTheory.measure_preimage_snd_singleton_eq_sum {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSingletonClass α] [MeasurableSpace β] [MeasurableSingletonClass β] [Fintype α] (μ : MeasureTheory.Measure (α × β)) (y : β) : μ (Prod.snd ⁻¹' {y}) = Finset.univ.sum fun (x : α) => μ {(x, y)}