Smallness of the DFinsupp type #
Let π : ι → Type v. If ι and all the π i are w-small, this provides a Small.{w}
instance on DFinsupp π.
instance
DFinsupp.small
{ι : Type u}
{π : ι → Type v}
[(i : ι) → Zero (π i)]
[Small.{w, u} ι]
[∀ (i : ι), Small.{w, v} (π i)]
: