∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α] [inst_2 : LinearOrder α]
  [OrderTopology α] [SecondCountableTopology α] {s : Set α}, (∀ x ∈ s, s ∈ nhdsWithin x (Set.Ioi x)) → MeasurableSet s