Closed set in well-order is closed under suprema

Stream: Is there code for X?

[Violeta Hernández]

Do we have anything like the following?

import Mathlib.Topology.Order.Basic

variable {α : Type*} [ConditionallyCompleteLinearOrder α] [WellFoundedLT α] [TopologicalSpace α] [OrderTopology α]

theorem sSup_mem_closure {s : Set α} (hn : s.Nonempty) (hs : BddAbove s) : sSup s ∈ closure s := by
  sorry

[Violeta Hernández]

docs#IsLUB.frequently_mem seems really close to this, but idk enough about the topology API to tell whether the conversion is immediate or not

[Jireh Loreaux]

docs#IsLUB.mem_closure is just below that.