Theorem Finsupp.support_mapDomain_of_nonneg

Modification history

2026-09-09 15:18
Mathlib/Data/Finsupp/Order.lean
feat(Data/Finsupp): support of `mapDomain` is image of support if nonneg (#43610) …
Added Finsupp.support_mapDomain_of_nonnegView on Github →