case refine'_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)

case refine'_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m = boundedBy (sInfGen m)
refine' le_antisymm _ _
case refine'_1
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
μ : OuterMeasure α
hμ : μ ∈ m
⊢ ↑(sInf m) s ≤ ↑μ s
case refine'_1
α : Type u_1
m : Set (OuterMeasure α)
⊢ sInf m ≤ boundedBy (sInfGen m)
refine' le_boundedBy.2 fun s => le_iInf₂ fun μ hμ => _
no goals
case refine'_1
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
μ : OuterMeasure α
hμ : μ ∈ m
⊢ ↑(sInf m) s ≤ ↑μ s
apply sInf_le hμ
case refine'_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ ∀ (b : OuterMeasure α), b ∈ m → boundedBy (sInfGen m) ≤ b
case refine'_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ boundedBy (sInfGen m) ≤ sInf m
refine' le_sInf _
case refine'_2
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
t : Set α
⊢ ↑(boundedBy (sInfGen m)) t ≤ ↑μ t
case refine'_2
α : Type u_1
m : Set (OuterMeasure α)
⊢ ∀ (b : OuterMeasure α), b ∈ m → boundedBy (sInfGen m) ≤ b
intro μ hμ t
no goals
case refine'_2
α : Type u_1
m : Set (OuterMeasure α)
μ : OuterMeasure α
hμ : μ ∈ m
t : Set α
⊢ ↑(boundedBy (sInfGen m)) t ≤ ↑μ t
refine' le_trans (boundedBy_le t) (iInf₂_le μ hμ)