Multisets of values indexed by Fin n

The multiset of values of a family i ↦ g i indexed by Fin n, through the coercion to ℕ, is the image of Multiset.range n under g (Fin.univ_val_map_eq_map_range). This is the multiset analogue of Fin.prod_univ_eq_prod_range, and lets a statement about a family indexed by Fin n be compared with one about an initial segment of ℕ without passing through lists.

theorem Fin.univ_val_map_eq_map_range {α : Type u_1} (g : ℕ → α) (n : ℕ) : Multiset.map (fun (i : Fin n) => g ↑i) Finset.univ.val = Multiset.map g (Multiset.range n)

The multiset of values g i for i : Fin n is the image of Multiset.range n under g.