English
Nodup(flatMap f l1) is equivalent to (forall x in l1, Nodup(f x)) and Pairwise (Disjoint on f) l1.
Русский
Безповторность flatMap f l1 эквивалентна тому, что для каждого элемента x из l1 выполнено Nodup(f x) и пары элементов x,y из l1 не пересекаются через f.
LaTeX
$$$\\operatorname{Nodup}(\\operatorname{flatMap} f l_1) \\iff (\\forall x \\in l_1, \\operatorname{Nodup}(f x)) \\land \\operatorname{Pairwise}(\\operatorname{Disjoint} \\text{ on } f) l_1$$$
Lean4
theorem nodup_flatMap {l₁ : List α} {f : α → List β} :
Nodup (l₁.flatMap f) ↔ (∀ x ∈ l₁, Nodup (f x)) ∧ Pairwise (Disjoint on f) l₁ :=
by
simp only [List.flatMap, nodup_flatten, pairwise_map, and_comm, mem_map, exists_imp, and_imp]
rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x) from
forall_swap.trans <| forall_congr' fun _ => forall_eq']
