no goals
α : Type u_1
m : Set (OuterMeasure α)
s : Set α
h : Set.Nonempty s
hm : m = ∅
⊢ ↑(sInf m) s = ⨅ (t : ℕ → Set α) (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ (μ : OuterMeasure α) (_ : μ ∈ m), ↑μ (t n)
simp [hm, h]