case h
α : Type u_1
β : Type ?u.697521
m : MeasurableSpace α
L : Type ?u.697527
M : Type u_2
N : Type ?u.697533
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(trim v (_ : n ≤ n)) i = ↑v i
α : Type u_1
β : Type ?u.697521
m : MeasurableSpace α
L : Type ?u.697527
M : Type u_2
N : Type ?u.697533
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
⊢ trim v (_ : n ≤ n) = v
ext1 i hi
no goals
case h
α : Type u_1
β : Type ?u.697521
m : MeasurableSpace α
L : Type ?u.697527
M : Type u_2
N : Type ?u.697533
inst✝⁵ : AddCommMonoid L
inst✝⁴ : TopologicalSpace L
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
n : MeasurableSpace α
v : VectorMeasure α M
i : Set α
hi : MeasurableSet i
⊢ ↑(trim v (_ : n ≤ n)) i = ↑v i
exact if_pos hi