α : Type u_2
β : Type u_1
γ : Type ?u.49088
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ x, ∀ (y : β), f x ≤ f y
α : Type u_2
β : Type u_1
γ : Type ?u.49088
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
⊢ ∃ x, ∀ (y : β), f x ≤ f y
inhabit β
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.49088
inst✝⁵ : ConditionallyCompleteLinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ x, ∀ (y : β), f x ≤ f y
exact hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)