sSup in closure

Stream: Is there code for X?

[Ira Fesefeldt]

I am still rather novice in topology, but I believe something like this holds? If yes, is there a proof for this in mathlib?

import Mathlib

lemma sSup_in_closure (s s' : Set ℝ) (h : s ⊆ s'): sSup s ∈ closure s' := by sorry

[Yaël Dillies]

You need to assume s is nonempty and bounded above

[Ira Fesefeldt]

Oh, yes.

[Ira Fesefeldt]

import Mathlib

lemma sSup_in_closure (s s' : Set ENNReal) (h : s ⊆ s'): sSup s ∈ closure s' := by sorry

Do I also need one of the assumptions if the domain is a CL?

[Ira Fesefeldt]

The answer is yes, I need nonemptyness:

import Mathlib

lemma sSup_in_closure (s s' : Set ENNReal) (h_nonempty : Set.Nonempty s) (h : s ⊆ s'): sSup s ∈ closure s' := by
  apply Set.mem_of_subset_of_mem (closure_mono h)
  exact sSup_mem_closure h_nonempty