∀ {α : Type u_2} {β : Type u_3} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [inst_2 : TopologicalSpace β] [ClosedIciTopology α] {f : β → α} {K : Set β},
  IsCompact K → K.Nonempty → ContinuousOn f K → ∀ (y : α), sSup (f '' K) < y ↔ ∀ x ∈ K, f x < y