A continuous function takes its minimum on ℝ × ℝ

Stream: Is there code for X?

[Michael Stoll]

...or, more generally, how do I get that a continuous real-valued function on a locally compact and complete space that gets large outside of a compact set has a minimum?

[Sébastien Gouëzel]

I typed exactly your sentence "a continuous real-valued function on a locally compact and complete space that gets large outside of a compact set has a minimum" in https://leansearch.net, and the second answer is docs#Continuous.exists_forall_le' which looks quite promising.

[Sébastien Gouëzel]

(or the version without a prime, a few lines below in the same file)

[Michael Stoll]

Thanks!
I had tried Loogle, but apparently did not hit on the right combination of search terms...

[Sébastien Gouëzel]

loogle is for when you can guess exactly the form of the lemma, while leansearch is more fuzzy in a sense. Both are extremely useful (to me, at least)!