case h
α : Type u_1
β : Type ?u.296719
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v : VectorMeasure α M
N : Type ?u.296766
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange v (AddMonoidHom.id M) (_ : Continuous id)) i✝ = ↑v i✝
α : Type u_1
β : Type ?u.296719
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v : VectorMeasure α M
N : Type ?u.296766
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
⊢ mapRange v (AddMonoidHom.id M) (_ : Continuous id) = v
ext
no goals
case h
α : Type u_1
β : Type ?u.296719
m inst✝⁵ : MeasurableSpace α
inst✝⁴ : MeasurableSpace β
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
v : VectorMeasure α M
N : Type ?u.296766
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange v (AddMonoidHom.id M) (_ : Continuous id)) i✝ = ↑v i✝
rfl