case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.35524
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set β
hs : IsCompact s
ne_s : Set.Nonempty s
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : ∀ (y : β), y ∈ s → f x ≤ f y
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
α : Type u_2
β : Type u_1
γ : Type ?u.35524
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set β
hs : IsCompact s
ne_s : Set.Nonempty s
f : β → α
hf : ContinuousOn f s
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
rcases hs.exists_sInf_image_eq_and_le ne_s hf with ⟨x, hxs, -, hx⟩
no goals
case intro.intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.35524
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
s : Set β
hs : IsCompact s
ne_s : Set.Nonempty s
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : ∀ (y : β), y ∈ s → f x ≤ f y
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
exact ⟨x, hxs, hx⟩