max over compact of continuous

Stream: Is there code for X?

[Yaël Dillies]

Has anyone already proven the fact that a continuous function reaches a maximum on any compact set?
Here's the precise statement I need

import data.real.basic
import algebra.module.linear_map
import analysis.convex.topology

variables {E : Type*} [normed_group E] [normed_space ℝ E] {A : set E}

lemma exists_max (l : E →L[ℝ] ℝ) (hAcomp : is_compact A) :
  {y ∈ A | ∀ z ∈ A, l z ≤ l y}.nonempty := sorry

[Kevin Buzzard]

You have to be careful because A could be empty

[Yaël Dillies]

Oh right! But that's fine, I do have this assumption in my drawers.

[Kevin Buzzard]

All you need is a continuous map from a nonempty compact subset of a topological space so that's the place to start looking

[Anatole Dedecker]

I can't find this exact theorem but it should be a mix of docs#is_compact.Sup_mem and docs#is_compact.image

[Anatole Dedecker]

Found ! docs#is_compact.exists_Sup_image_eq

[Yaël Dillies]

Great! Seems like docs#is_compact.exists_forall_ge is exactly what I need.