English
Let f be a family of subsets indexed by ι and S ⊆ ι. The family {f(i)}_{i∈S} is pairwise disjoint if and only if for all i, j ∈ S, the intersection f(i) ∩ f(j) is nonempty only when i = j.
Русский
Пусть f — семейство подмножеств, индексированное по ι, и S ⊆ ι. Семейство {f(i)}_{i∈S} попарно непересекается тогда и только тогда, когда для любых i, j ∈ S пересечение f(i) ∩ f(j) непусто только если i = j.
LaTeX
$$$\\displaystyle \\bigl(\\forall i\\in s, \\forall j\\in s, (f(i) \\cap f(j)) = \\emptyset \\bigr) \\ \\Longleftrightarrow\\ \\bigl(\\forall i\\in s, \\forall j\\in s, (f(i) \\cap f(j)) \\neq \\emptyset \\Rightarrow i = j\\bigr)$$$
Lean4
theorem pairwiseDisjoint_iff : 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]
