English
Let s be a multiset of elements of α and f: α → Multiset β. Then the multiset bind (s.bind f) has no duplicates if and only if (i) for every a in s, the multiset f(a) has no duplicates, and (ii) the family {f(a) : a ∈ s} is pairwise disjoint.
Русский
Пусть s — мульти-множество элементов α и f: α → Multiset β. Тогда связанное мульти-множество (s.bind f) не содержит повторов тогда и только тогда, когда (i) для каждого a ∈ s множество f(a) без повторов, и (ii) семейство {f(a) : a ∈ s} попарно несовместимо.
LaTeX
$$$ \operatorname{Nodup}(\mathrm{bind}(s,f)) \iff \left( \forall a \in s, \operatorname{Nodup}(f(a)) \right) \land s.\operatorname{Pairwise}(\operatorname{Disjoint} \circ f)$$$
Lean4
@[simp]
theorem nodup_bind : Nodup (bind s f) ↔ (∀ a ∈ s, Nodup (f a)) ∧ s.Pairwise (Disjoint on f) :=
by
have : ∀ a, ∃ l : List β, f a = l := fun a => Quot.induction_on (f a) fun l => ⟨l, rfl⟩
choose f' h' using this
have : f = fun a ↦ ofList (f' a) := funext h'
have hd : Symmetric fun a b ↦ List.Disjoint (f' a) (f' b) := fun a b h ↦ h.symm
exact
Quot.induction_on s <| by
unfold Function.onFun
simp [this, List.nodup_flatMap, pairwise_coe_iff_pairwise hd]
