Commit 2024-07-09 05:38 a90eae70

View on Github →

feat(Data/ENat): sSup_eq_zero and sInf_eq_zero (#14043) To make working with ENat easier.

Estimated changes

Modified Mathlib/Data/ENat/Basic.lean

added theorem ENat.lt_one_iff_eq_zero

Modified Mathlib/Data/ENat/Lattice.lean

added theorem ENat.sInf_eq_zero

added theorem ENat.sSup_eq_zero'

added theorem ENat.sSup_eq_zero

Modified Mathlib/Order/CompleteLattice.lean

added theorem sSup_eq_bot'