Theorem ENat.le_iInf₂_add_iInf₂

Modification history

2026-03-10 22:48
Mathlib/Data/ENat/Lattice.lean
feat(ENat): relate iInf of ENats to addition (#36452) …
Added ENat.le_iInf₂_add_iInf₂View on Github →