∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ]
  {f : α → γ}, UpperSemicontinuousWithinAt f s x → Filter.limsup f (nhdsWithin x s) ≤ f x