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