α : Type u_2
β✝ : Type ?u.913715
γ : Type ?u.913718
δ : Type ?u.913721
m : MeasurableSpace α
inst✝² : Zero β✝
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β✝
β : Type u_1
inst✝ : AddMonoid β
f g : α →ₛ β
hf : SimpleFunc.FinMeasSupp f μ
hg : SimpleFunc.FinMeasSupp g μ
⊢ SimpleFunc.FinMeasSupp (map (fun p => p.fst + p.snd) (pair f g)) μ
α : Type u_2
β✝ : Type ?u.913715
γ : Type ?u.913718
δ : Type ?u.913721
m : MeasurableSpace α
inst✝² : Zero β✝
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β✝
β : Type u_1
inst✝ : AddMonoid β
f g : α →ₛ β
hf : SimpleFunc.FinMeasSupp f μ
hg : SimpleFunc.FinMeasSupp g μ
⊢ SimpleFunc.FinMeasSupp (f + g) μ
rw [add_eq_map₂]
no goals
α : Type u_2
β✝ : Type ?u.913715
γ : Type ?u.913718
δ : Type ?u.913721
m : MeasurableSpace α
inst✝² : Zero β✝
inst✝¹ : Zero γ
μ : Measure α
f✝ : α →ₛ β✝
β : Type u_1
inst✝ : AddMonoid β
f g : α →ₛ β
hf : SimpleFunc.FinMeasSupp f μ
hg : SimpleFunc.FinMeasSupp g μ
⊢ SimpleFunc.FinMeasSupp (map (fun p => p.fst + p.snd) (pair f g)) μ
exact hf.map₂ hg (zero_add 0)