English
For a function f: α → β and a finite set t ⊆ α, the family of fibers t.filter (f · = x) indexed by x in s is pairwise disjoint as sets in α; i.e., the pieces of t where f takes a fixed value are disjoint for different values.
Русский
Для функции f: α → β и множества t ⊆ α пара одинаковых значений функции образуются непересекающимися частями.
LaTeX
$$Set.pairwiseDisjoint (\\n f : α → β) (s : Set β) (t : Finset α) : s.\\PairwiseDisjoint (fun x ↦ t.filter (f · = x))$$
Lean4
theorem _root_.Set.pairwiseDisjoint_filter [DecidableEq β] (f : α → β) (s : Set β) (t : Finset α) :
s.PairwiseDisjoint fun x ↦ t.filter (f · = x) :=
by
rintro i - j - h u hi hj x hx
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = i := by simpa using hi hx
obtain ⟨-, rfl⟩ : x ∈ t ∧ f x = j := by simpa using hj hx
contradiction
