∀ {α : Type u_5} {E : Type u_6} {m m₂ : MeasurableSpace α} [inst : TopologicalSpace E] [inst_1 : Zero E] {s : Set α}
  {f : α → E},
  MeasurableSet s →
    (∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)) →
      MeasureTheory.StronglyMeasurable f → (∀ x ∉ s, f x = 0) → MeasureTheory.StronglyMeasurable f