English
We say s is PairwiseDisjoint under f when the images f i are pairwise disjoint for i in s.
Русский
Говорят, что множество s попарно непересекается относительно f, если образы f(i) для разных i в s непересекаются.
LaTeX
$$PairwiseDisjoint (s,f) := s.Pairwise (Disjoint on f)$$
Lean4
/-- A set is `PairwiseDisjoint` under `f`, if the images of any distinct two elements under `f`
are disjoint.
`s.Pairwise Disjoint` is (definitionally) the same as `s.PairwiseDisjoint id`. We prefer the latter
in order to allow dot notation on `Set.PairwiseDisjoint`, even though the former unfolds more
nicely. -/
def PairwiseDisjoint (s : Set ι) (f : ι → α) : Prop :=
s.Pairwise (Disjoint on f)
