no goals
α : Type u_2
β : Type u_1
γ : Type ?u.46391
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : β → α
hf : Continuous f
x₀ : β
h : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
⊢ ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 univ, f x₀ ≤ f x
rwa [principal_univ, inf_top_eq]