α : Type u_1
β : Type ?u.103430
R : Type ?u.103433
R' : Type ?u.103436
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ ↑m (u ∩ s) ≤ ↑m' (u ∩ t)
α : Type u_1
β : Type ?u.103430
R : Type ?u.103433
R' : Type ?u.103436
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ ↑(↑(restrict s) m) u ≤ ↑(↑(restrict t) m') u
simp only [restrict_apply]
no goals
α : Type u_1
β : Type ?u.103430
R : Type ?u.103433
R' : Type ?u.103436
ms : Set (OuterMeasure α)
m✝ : OuterMeasure α
s t : Set α
h : s ⊆ t
m m' : OuterMeasure α
hm : m ≤ m'
u : Set α
⊢ ↑m (u ∩ s) ≤ ↑m' (u ∩ t)
exact (hm _).trans (m'.mono <| inter_subset_inter_right _ h)