Theorem ENat.sSup_eq_top_of_infinite

Modification history

2024-07-31 14:10
Mathlib/Data/ENat/Lattice.lean
feat(ENat): sSup_mem_of_Nonempty_of_lt_top (#15347) …
Added ENat.sSup_eq_top_of_infiniteView on Github →