Theorem ENat.coe_iInf

Modification history

2024-06-11 23:44

Mathlib/Data/ENat/Lattice.lean

chore: fix junk value for `sInf` on `WithTop` (#13717) …

Modified ENat.coe_iInf View on Github →

2023-09-04 13:19

Mathlib/Data/ENat/Lattice.lean

feat: More complete lattice `WithTop` lemmas (#6947) …

Added ENat.coe_iInf View on Github →