English
Let l be a noduplicated list of indices and f a mapping from indices to a partially ordered set with a bottom element. Then the finite set of indices l induces a family {f(i) : i ∈ l}; this family is pairwise disjoint if and only if, when viewed as a list, the elements {f(i)} are pairwise disjoint in the sense that for any i ≠ j in l, f(i) and f(j) are disjoint.
Русский
Пусть l — список без повторов индексов; для отображения f: индексы → α. Тогда семейство {f(i) : i ∈ l} попарно дизъюнктивно тогда и только тогда, когда как список [i] элементы f(i) попарно дизъюнктивны, то есть для любых i ≠ j в l верно Disjoint(f(i), f(j)).
LaTeX
$$$ (l^{\\mathrm{toFinset}}) .\\mathrm{PairwiseDisjoint} f \\;\\Longleftrightarrow\\; l .\\mathrm{Pairwise} ( \\lambda i j, \\operatorname{Disjoint}(f(i), f(j)) ). $$$
Lean4
theorem pairwiseDisjoint_iff_coe_toFinset_pairwise_disjoint {α ι} [PartialOrder α] [OrderBot α] [DecidableEq ι]
{l : List ι} {f : ι → α} (hn : l.Nodup) :
(l.toFinset : Set ι).PairwiseDisjoint f ↔ l.Pairwise (_root_.Disjoint on f) :=
pairwise_iff_coe_toFinset_pairwise hn (symmetric_disjoint.comap f)
