Theorem ENat.iInf_eq_coe_iff

Modification history

2026-07-17 11:15
Mathlib/Data/ENat/Lattice.lean
chore(Data/ENat): replace `coe` with `natCast` in lemma names (#41140) …
Deleted ENat.iInf_eq_coe_iffView on Github →
2026-04-02 16:35
Mathlib/Data/ENat/Lattice.lean
feat(Data/ENat): add lemma `ENat.iInf_eq_coe_iff` (#34144)
Added ENat.iInf_eq_coe_iffView on Github →