## Stream: Is there code for X?

### Topic: max over compact of continuous

#### Yaël Dillies (Apr 15 2021 at 06:59):

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 (Apr 15 2021 at 07:00):

You have to be careful because A could be empty

#### Yaël Dillies (Apr 15 2021 at 07:01):

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

#### Kevin Buzzard (Apr 15 2021 at 07:02):

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 (Apr 15 2021 at 07:30):

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

#### Yaël Dillies (Apr 15 2021 at 07:35):

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

Last updated: May 19 2021 at 00:40 UTC