α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
this : (fun s => ⨆ (_ : Set.Nonempty s), m s) = m
⊢ ↑(boundedBy m) s = ↑(OuterMeasure.ofFunction m m_empty) s
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ ↑(boundedBy m) s = ↑(OuterMeasure.ofFunction m m_empty) s
have : (fun s : Set α => ⨆ _ : s.Nonempty, m s) = m := by
  ext1 t
  cases' t.eq_empty_or_nonempty with h h <;> simp [h, Set.not_nonempty_empty, m_empty]
no goals
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
this : (fun s => ⨆ (_ : Set.Nonempty s), m s) = m
⊢ ↑(boundedBy m) s = ↑(OuterMeasure.ofFunction m m_empty) s
simp [boundedBy, this]
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ (⨆ (_ : Set.Nonempty t), m t) = m t
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s : Set α
⊢ (fun s => ⨆ (_ : Set.Nonempty s), m s) = m
ext1 t
no goals
case h
α : Type u_1
m : Set α → ℝ≥0∞
m_empty : m ∅ = 0
s t : Set α
⊢ (⨆ (_ : Set.Nonempty t), m t) = m t
cases' t.eq_empty_or_nonempty with h h <;> simp [h, Set.not_nonempty_empty, m_empty]