rintro b ⟨x, hx, rfl⟩
case h
α : 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 : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ f a ∈ lowerBounds (f '' s)
case h.intro.intro
α : 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 : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x