Closed gebner closed 2 years ago
theorem _root_.continuous.exists_forall_le [Nonempty β] {f : β → α} (hf : Continuous f) (hlim : Tendsto f (cocompact β) atTop) : ∃ x, ∀ y, f x ≤ f y := by
This is implemented upstream now: https://github.com/leanprover/lean4/issues/490