English
If a list l1 is nodup and for every a in l1 the corresponding list l2(a) is nodup, then the dependent product list (sigma) is nodup.
Русский
Если список l1 не содержит повторов и для каждого элемента a списка l1 соответствующий список l2(a) также не содержит повторов, то зависимое произведение (сигма-образование) без повторов.
LaTeX
$$$ \\operatorname{Nodup}(l_1) \\land \\forall a\\in l_1, \\operatorname{Nodup}(l_2(a)) \\Rightarrow \\operatorname{Nodup}\\bigl\\{(a,b) \\mid a \\in l_1 \\wedge b \\in l_2(a)\\bigr\\}. $$$
Lean4
theorem sigma {σ : α → Type*} {l₂ : ∀ a, List (σ a)} (d₁ : Nodup l₁) (d₂ : ∀ a, Nodup (l₂ a)) : (l₁.sigma l₂).Nodup :=
nodup_flatMap.2
⟨fun a _ => (d₂ a).map fun b b' h => by injection h with _ h,
d₁.imp fun {a₁ a₂} n x h₁ h₂ => by
rcases mem_map.1 h₁ with ⟨b₁, _, rfl⟩
rcases mem_map.1 h₂ with ⟨b₂, mb₂, ⟨⟩⟩
exact n rfl⟩
