Commit 2024-07-31 14:10 61c938b7
View on Github →feat(ENat): sSup_mem_of_Nonempty_of_lt_top (#15347) Lemma statement due to Gareth Ma. More discussion at https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/ENat.2EiSup_eq_coe_iff from the Carleson project