simp only [h, Set.image_empty]
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow (f '' s)
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow ∅