Theorem ENat.lt_one_iff_eq_zero

Modification history

2024-07-09 05:38
Mathlib/Data/ENat/Basic.lean
feat(Data/ENat): `sSup_eq_zero` and `sInf_eq_zero` (#14043) …
Added ENat.lt_one_iff_eq_zeroView on Github →