α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ↑(trim m) s = ⨅ (t : Set α) (_ : MeasurableSet t) (_ : s ⊆ t), ↑m t
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ↑(trim m) s = ⨅ (t : Set α) (_ : s ⊆ t) (_ : MeasurableSet t), ↑m t
simp (config := { singlePass := true }) only [iInf_comm]
no goals
α : Type u_1
inst✝ : MeasurableSpace α
m : OuterMeasure α
s : Set α
⊢ ↑(trim m) s = ⨅ (t : Set α) (_ : MeasurableSet t) (_ : s ⊆ t), ↑m t
exact
  inducedOuterMeasure_eq_iInf MeasurableSet.iUnion (fun f _ => m.iUnion_nat f)
    (fun _ _ _ _ h => m.mono h) s