∀ {α : Type u_4} {β : Type u_5} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f g : α → β} {s : Set α} {a : α},
  UpperSemicontinuousWithinAt f s a →
    UpperSemicontinuousWithinAt g s a → UpperSemicontinuousWithinAt (fun x => min (f x) (g x)) s a