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