∀ {α : Type u_1} [inst : TopologicalSpace α] {γ : Type u_4} [inst_1 : LinearOrder γ] [inst_2 : TopologicalSpace γ]
  [ClosedIicTopology γ] {f : α → γ}, UpperSemicontinuous f → IsClosed {p | p.2 ≤ f p.1}