English
If two lists have no duplicates, then their Cartesian product (the list of all pairs (a,b) with a from the first list and b from the second) also has no duplicates.
Русский
Если два списка не содержат повторяющихся элементов, то их декартово произведение (список всех пар (a,b), где a взято из первого списка, b — из второго) также не содержит повторов.
LaTeX
$$$ \\operatorname{Nodup}(l_1) \\land \\operatorname{Nodup}(l_2) \\Rightarrow \\operatorname{Nodup}\\bigl(\\{(a,b) \\mid a \\in l_1 \\wedge b \\in l_2\\}\\bigr). $$$
Lean4
protected theorem product {l₂ : List β} (d₁ : l₁.Nodup) (d₂ : l₂.Nodup) : (l₁ ×ˢ l₂).Nodup :=
nodup_flatMap.2
⟨fun a _ => d₂.map <| LeftInverse.injective fun b => (rfl : (a, b).2 = b),
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⟩
