Theorem ENat.finite_of_sSup_lt_top

Modification history

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