Permutations from the maps of lists without duplicates

Candidates for Mathlib.Data.List.Nodup, next to List.Nodup.map_on and List.nodup_flatMap: a list without duplicates, mapped by a function that is injective on it, is a permutation of every list without duplicates whose members are the images; and a concatenation l.flatMap f has no duplicates when the member of l that gives an entry can be read off the entry.

Main statements

• List.perm_map_of_nodup: the map of a list without duplicates by a function injective on it is a permutation of every list without duplicates with the same members.
• List.Nodup.flatMap: l.flatMap f has no duplicates when l and each f a have none and a is a function of each entry of f a.

theorem List.perm_map_of_nodup {α : Type u_1} {β : Type u_2} {l : List α} {l' : List β} {f : α → β} (hl : l.Nodup) (hl' : l'.Nodup) (hf : ∀ (x : α), x ∈ l → ∀ (y : α), y ∈ l → f x = f y → x = y) (h : ∀ (b : β), b ∈ l' ↔ ∃ (a : α), a ∈ l ∧ f a = b) : (map f l).Perm l'

A list without duplicates, mapped by a function that is injective on it, is a permutation of every list without duplicates whose members are exactly the images; compare List.perm_ext_iff_of_nodup and List.Nodup.map_on.

theorem List.Nodup.flatMap {α : Type u_1} {β : Type u_2} {l : List α} {f : α → List β} (hl : l.Nodup) (hf : ∀ (a : α), a ∈ l → (f a).Nodup) (g : β → α) (hg : ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → g b = a) : (flatMap f l).Nodup

A concatenation l.flatMap f has no duplicates when l and each f a have none and the member a of l can be read off each entry of f a by a function g, so that the lists f a are disjoint; compare List.nodup_flatMap.