Continuous function reaches its supremum on a dense set

Stream: Is there code for X?

[Yongxi Lin (Aaron)]

import Mathlib

variable {ι : Type*} {f : ι → ℝ} [TopologicalSpace ι]

theorem continuous_supremum_dense {S : Set ι} (hS : Dense S) (hf : Continuous f):
    ⨆ i, f i = ⨆ s : S, f s := by sorry

Probably one can generalize this to the case that the codomain of f is endowed with an order topology.

[Kevin Buzzard]

I would have thought that ⨆ s ∈ S, f s was more idiomatic.

[Anatole Dedecker]

Kevin Buzzard said:

I would have thought that ⨆ s ∈ S, f s was more idiomatic.

It is false though, right?

[Yongxi Lin (Aaron)]

Anatole Dedecker said:

Kevin Buzzard said:

I would have thought that ⨆ s ∈ S, f s was more idiomatic.

It is false though, right?

May you explain further why my statement is false? I probably should include more assumptions.

[Kevin Buzzard]

The best way is to just try and prove it yourself and see where things start to go wrong. Firstly, do understand that the ⨆ of an unbounded set is zero? Do you mean to allow this?

[Yongxi Lin (Aaron)]

Yes, and both sides should be equal to zero if f is unbounded.

[Anatole Dedecker]

Sorry, I meant that Kevin's phrasing was wrong. Because ⨆ s ∈ S, f s is really ⨆ s, ⨆ (h : s ∈ S), f s, which is never what you want. I believe your initial statement though, even in the unbounded case.

[Kevin Buzzard]

aah yes apologies, this is a gotcha.

[Kevin Buzzard]

yes I believe the original statement and I now see that my modification might not be true.

[Anatole Dedecker]

I can't find the result though

[Jireh Loreaux]

I don't think we have it. I would probably try to get it using docs#isLUB_iff_of_subset_of_subset_closure and docs#Continuous.range_subset_closure_image_dense along with some glue to go from iSup to IsLUB.

[Aaron Liu]

Probably the assumption here is docs#SupConvergenceClass

[Aaron Liu]

For the generalization, I mean

[Jireh Loreaux]

You should be able to remove the BddAbove hypothesis too in a docs#ConditionallyCompleteLinearOrder using docs#BddAbove.closure and the junk value constraint docs#ConditionallyCompleteLinearOrder.csSup_of_not_bddAbove

import Mathlib

open Set

variable {ι α : Type*} [ConditionallyCompleteLattice α] [TopologicalSpace α]
  [ClosedIicTopology α] {f : ι → α} [TopologicalSpace ι]

theorem continuous_supremum_dense {S : Set ι} (hS : Dense S) (hf : Continuous f)
    (h : BddAbove (range f)) :
    ⨆ i, f i = ⨆ s : S, f s := by
  rw [← sSup_range, ← sSup_range]
  obtain (_ | _) := isEmpty_or_nonempty ι
  · simp [Set.range_eq_empty]
  have h₂ : Nonempty S := hS.nonempty.to_subtype
  refine (isLUB_csSup (range_nonempty f) h).unique ?_
  rw [← isLUB_iff_of_subset_of_subset_closure (image_subset_range f S)
    (hf.range_subset_closure_image_dense hS)]
  simpa [← Function.comp_def, range_comp] using
    isLUB_csSup (range_nonempty (fun x : S ↦ f x)) <| h.mono <| range_comp_subset_range ..

[Yongxi Lin (Aaron)]

@Jireh Loreaux Thank you for your code! :thank_you: