α : Type u_1
β : Type ?u.152195
γ : Type ?u.152198
δ : Type ?u.152201
ι : Type ?u.152204
R : Type ?u.152207
R' : Type ?u.152210
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
h : ∀ (μ' : Measure α), μ' ∈ m → μ ≤ μ'
this : ↑μ ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s ≤ ↑(sInf (toOuterMeasure '' m)) s
α : Type u_1
β : Type ?u.152195
γ : Type ?u.152198
δ : Type ?u.152201
ι : Type ?u.152204
R : Type ?u.152207
R' : Type ?u.152210
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
h : ∀ (μ' : Measure α), μ' ∈ m → μ ≤ μ'
this : ↑μ ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s ≤ ↑↑(sInf m) s
rw [sInf_apply hs]
no goals
α : Type u_1
β : Type ?u.152195
γ : Type ?u.152198
δ : Type ?u.152201
ι : Type ?u.152204
R : Type ?u.152207
R' : Type ?u.152210
m0 : MeasurableSpace α
inst✝¹ : MeasurableSpace β
inst✝ : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s✝ s' t : Set α
m : Set (Measure α)
h : ∀ (μ' : Measure α), μ' ∈ m → μ ≤ μ'
this : ↑μ ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ ↑↑μ s ≤ ↑(sInf (toOuterMeasure '' m)) s
exact this s