cases s.eq_empty_or_nonempty with
| inl h =>
    simp only [h, Set.image_empty]
    exact bddBelow_empty
| inr h =>
    obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact h hs hf
    use f a
    rintro b ⟨x, hx, rfl⟩; exact has x hx
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ BddBelow (f '' s)
no goals