Theorem ENat.exists_eq_iInf

Modification history

2025-04-11 01:58
Mathlib/Data/ENat/Lattice.lean
chore(Data/ENat): golf `exists_eq_iInf` (#23931) …
Modified ENat.exists_eq_iInfView on Github →
2025-03-31 10:57
Mathlib/Data/ENat/Lattice.lean
feat(Data/ENat): multiplication and Inf/Sup lemmas (#23454) …
Added ENat.exists_eq_iInfView on Github →