case h
α : Type u_2
β : Type u_1
γ : Type ?u.348297
δ : Type ?u.348300
ι : Type ?u.348303
R : Type ?u.348306
R' : Type ?u.348309
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
α : Type u_2
β : Type u_1
γ : Type ?u.348297
δ : Type ?u.348300
ι : Type ?u.348303
R : Type ?u.348306
R' : Type ?u.348309
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
⊢ map f μ = sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b
ext1 s hs
case h
α : Type u_2
β : Type u_1
γ : Type ?u.348297
δ : Type ?u.348300
ι : Type ?u.348303
R : Type ?u.348306
R' : Type ?u.348309
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
this : ∀ (y : β), y ∈ s → MeasurableSet (f ⁻¹' {y})
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
case h
α : Type u_2
β : Type u_1
γ : Type ?u.348297
δ : Type ?u.348300
ι : Type ?u.348303
R : Type ?u.348306
R' : Type ?u.348309
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
have : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y}) := fun y _ => hf (measurableSet_singleton _)
no goals
case h
α : Type u_2
β : Type u_1
γ : Type ?u.348297
δ : Type ?u.348300
ι : Type ?u.348303
R : Type ?u.348306
R' : Type ?u.348309
m0 : MeasurableSpace α
inst✝³ : MeasurableSpace β
inst✝² : MeasurableSpace γ
μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
inst✝¹ : Countable β
inst✝ : MeasurableSingletonClass β
μ : Measure α
f : α → β
hf : Measurable f
s : Set β
hs : MeasurableSet s
this : ∀ (y : β), y ∈ s → MeasurableSet (f ⁻¹' {y})
⊢ ↑↑(map f μ) s = ↑↑(sum fun b => ↑↑μ (f ⁻¹' {b}) • dirac b) s
simp [← tsum_measure_preimage_singleton (to_countable s) this, *,
  tsum_subtype s fun b => μ (f ⁻¹' {b}), ← indicator_mul_right s fun b => μ (f ⁻¹' {b})]