theorem MeasureTheory.Measure.ennreal_smul_real_apply {Ω : Type u_4} {x✝ : MeasurableSpace Ω} (c : ENNReal) (μ : Measure Ω) (s : Set Ω) : (c • μ).real s = c.toReal • μ.real s

theorem MeasureTheory.Measure.nnreal_smul_real_apply {Ω : Type u_4} {x✝ : MeasurableSpace Ω} (c : NNReal) (μ : Measure Ω) (s : Set Ω) : (c • μ).real s = c • μ.real s

theorem MeasureTheory.Measure.comap_real_apply {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} {s : Set α} {f : α → β} (hfi : Function.Injective f) (hf : ∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) (hs : MeasurableSet s) : (comap f μ).real s = μ.real (f '' s)

theorem MeasureTheory.Measure.prod_real_singleton {α : Type u_1} {β : Type u_2} {x✝ : MeasurableSpace α} {x✝¹ : MeasurableSpace β} (μ : Measure α) (ν : Measure β) [SigmaFinite ν] (x : α × β) : (μ.prod ν).real {x} = μ.real {x.1} * ν.real {x.2}

theorem MeasureTheory.measureReal_preimage_fst_singleton_eq_sum {Ω : Type u_4} {Ω' : Type u_5} {x✝ : MeasurableSpace Ω} {x✝¹ : MeasurableSpace Ω'} [MeasurableSingletonClass Ω] [MeasurableSingletonClass Ω'] [Fintype Ω'] (μ : Measure (Ω × Ω')) [IsFiniteMeasure μ] (x : Ω) : μ.real (Prod.fst ⁻¹' {x}) = ∑ y : Ω', μ.real {(x, y)}

theorem MeasureTheory.measureReal_preimage_snd_singleton_eq_sum {Ω : Type u_4} {Ω' : Type u_5} {x✝ : MeasurableSpace Ω} {x✝¹ : MeasurableSpace Ω'} [MeasurableSingletonClass Ω] [MeasurableSingletonClass Ω'] [Fintype Ω] (μ : Measure (Ω × Ω')) [IsFiniteMeasure μ] (y : Ω') : μ.real (Prod.snd ⁻¹' {y}) = ∑ x : Ω, μ.real {(x, y)}