Commit 2026-03-10 22:48 6a9cd49a
View on Github →feat(ENat): relate iInf of ENats to addition (#36452) There are currently virtually no lemmas in mathlib relating the infimum of extended natural numbers to their addition: https://loogle.lean-lang.org/?q=ENat%2C+iInf%2C+_+%2B+_. This PR adds a collection, adapted from the analogous ones for ENNReal. In each case, the name (and proof) is picked to match that for ENNReal.