nat.exists_eq_supr

Stream: Is there code for X?

[Andrew Yang]

What is the best way to show this?

example {α : Type*} [nonempty α] (f : α → ℕ) (h : bdd_above (set.range f)) : ∃ i : α, f i = supr f := sorry

[Kevin Buzzard]

Alpha could be empty, right?

[Andrew Yang]

Ah yes. Fixed.

[Yaël Dillies]

docs#nat.Sup_mem

[Andrew Yang]

Thanks!