Mathlib Changelog
v4
Changelog
About
Github
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_top
View on Github →