α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), ↑μ a ≤ m a ↔ Set.Nonempty a → ↑μ a ≤ m a
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ μ ≤ boundedBy m ↔ ∀ (s : Set α), Set.Nonempty s → ↑μ s ≤ m s
rw [le_boundedBy, forall_congr']
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ ↑μ s ≤ m s ↔ Set.Nonempty s → ↑μ s ≤ m s
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
⊢ ∀ (a : Set α), ↑μ a ≤ m a ↔ Set.Nonempty a → ↑μ a ≤ m a
intro s
no goals
α : Type u_1
m : Set α → ℝ≥0∞
μ : OuterMeasure α
s : Set α
⊢ ↑μ s ≤ m s ↔ Set.Nonempty s → ↑μ s ≤ m s
cases' s.eq_empty_or_nonempty with h h <;> simp [h]