English
A family f indexed by a set s is pairwise disjoint if and only if for all i,j ∈ s, if f(i) ∩ f(j) is nonempty, then i = j.
Русский
Семейство, индексируемое множеством s, попарно непересекается тогда и только тогда, когда для любых i, j из s пересечение f(i) и f(j) непусто только если i = j.
LaTeX
$$$$ \text{Set.PairwiseDisjoint } f \iff \forall i\in S, \forall j\in S, (f(i) \cap f(j)).\mathrm{Nonempty} \Rightarrow i = j. $$$$
Lean4
theorem pairwiseDisjoint_iff {ι : Type*} {s : Set ι} {f : ι → Finset α} :
s.PairwiseDisjoint f ↔ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → (f i ∩ f j).Nonempty → i = j := by
simp [Set.PairwiseDisjoint, Set.Pairwise, Function.onFun, not_imp_comm (a := _ = _), not_disjoint_iff_nonempty_inter]
