IsGreatest of BddAbove

Stream: Is there code for X?

[Moritz Firsching]

I was wondering if the following (or some suitable generalization) is already in mathlib and I just didn't find it:

import Mathlib

theorem IsGreatest_of_BddAbove (S : Set ℕ) (h1 : S.Nonempty) (h2 : BddAbove S) :
    ∃ k, IsGreatest S k :=
  ⟨sSup S, ⟨Nat.sSup_mem h1 h2, fun x hx =>ConditionallyCompleteLattice.le_csSup S x h2 hx⟩⟩

[Ruben Van de Velde]

Maybe docs#IsClosed.isGreatest_csSup ?

[Ruben Van de Velde]

import Mathlib

theorem IsGreatest_of_BddAbove (S : Set ℕ) (h1 : S.Nonempty) (h2 : BddAbove S) :
    ∃ k, IsGreatest S k :=
  ⟨_, (isClosed_discrete _).isGreatest_csSup h1 h2⟩

[Yaël Dillies]

No need to invoke topology, though

[Yaël Dillies]

Doesn't seem like we have it explicitly, but Ruben is right that the correct lemma to have is not yours but s.Nonempty → BddAbove s → IsGreatest s (sSup s)

[Ruben Van de Velde]

More interesting is what's the right type class

[Yaël Dillies]

ConditionallyCompleteLattice + LocallyFiniteOrder