case h
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
⊢ MeasurableSet j → ↑(restrict (trim v hle) i) j = ↑(trim (restrict v i) hle) j
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
⊢ restrict (trim v hle) i = trim (restrict v i) hle
ext j
case h
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (trim v hle) i) j = ↑(trim (restrict v i) hle) j
case h
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
⊢ MeasurableSet j → ↑(restrict (trim v hle) i) j = ↑(trim (restrict v i) hle) j
intro hj
case h.hi
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet (j ∩ i)

case h.hi
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

case h.hi
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
case h
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ ↑(restrict (trim v hle) i) j = ↑(trim (restrict v i) hle) j
rw [@restrict_apply _ m, trim_measurableSet_eq hle hj, restrict_apply, trim_measurableSet_eq]
no goals
case h.hi
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet (j ∩ i)

case h.hi
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j

case h.hi
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet i

case h.hj
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
all_goals measurability
no goals
case h.hj
α : Type u_1
β : Type ?u.698391
m : MeasurableSpace α
L : Type ?u.698397
M : Type u_2
N : Type ?u.698403
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
j : Set α
hj : MeasurableSet j
⊢ MeasurableSet j
measurability