Zulip Chat Archive

Stream: Is there code for X?

Topic: max over compact of continuous


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 15 2021 at 07:00):

You have to be careful because A could be empty

view this post on Zulip Yaël Dillies (Apr 15 2021 at 07:01):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Anatole Dedecker (Apr 15 2021 at 07:33):

Found ! docs#is_compact.exists_Sup_image_eq

view this post on Zulip 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