English
Let l be a list of dependent pairs l = [⟨a_i, b_i⟩] with distinct keys (NodupKeys). Then the first components are pairwise distinct: for any s, t in l with s ≠ t, we have s.1 ≠ t.1. Equivalently, the sequence of first components is pairwise different.
Русский
Пусть l — список зависимых пар l = [⟨a_i, b_i⟩] с уникальными ключами (NodupKeys). Тогда первые компоненты попарно различны: для любых двух элементов списка s, t выполняется s.1 ≠ t.1.
LaTeX
$$$ \\mathrm{NodupKeys}(l) \\implies \\mathrm{Pairwise}\\bigl(\\lambda s,t:\\Sigma\\beta.\\; s.1 \\neq t.1\\bigr)\\, l $$$
Lean4
theorem pairwise_ne {l} (h : NodupKeys l) : Pairwise (fun s s' : Sigma β => s.1 ≠ s'.1) l :=
nodupKeys_iff_pairwise.1 h
