The composition of f : β₁ → β₂ and g : Π₀ i, β₁ i is map_range f hf g : Π₀ i, β₂ i, well defined when f 0 = 0.

filter p f is the function which is f i if p i is true and 0 otherwise.

subtype_domain p f is the restriction of the finitely supported function f to the subtype p.

sum f g is the sum of g i (f i) over the support of f.

prod f g is the product of g i (f i) over the support of f.