# Relations holding pairwise #

This file develops pairwise relations and defines pairwise disjoint indexed sets.

We also prove many basic facts about Pairwise. It is possible that an intermediate file, with more imports than Logic.Pairwise but not importing Data.Set.Function would be appropriate to hold many of these basic facts.

## Main declarations #

• Set.PairwiseDisjoint: s.PairwiseDisjoint f states that images under f of distinct elements of s are either equal or Disjoint.

## Notes #

The spelling s.PairwiseDisjoint id is preferred over s.Pairwise Disjoint to permit dot notation on Set.PairwiseDisjoint, even though the latter unfolds to something nicer.

theorem pairwise_on_bool {α : Type u_1} {r : ααProp} (hr : ) {a : α} {b : α} :
Pairwise (r on fun (c : Bool) => bif c then a else b) r a b
theorem pairwise_disjoint_on_bool {α : Type u_1} [] [] {a : α} {b : α} :
Pairwise (Disjoint on fun (c : Bool) => bif c then a else b) Disjoint a b
theorem Symmetric.pairwise_on {α : Type u_1} {ι : Type u_4} {r : ααProp} [] (hr : ) (f : ια) :
Pairwise (r on f) ∀ ⦃m n : ι⦄, m < nr (f m) (f n)
theorem pairwise_disjoint_on {α : Type u_1} {ι : Type u_4} [] [] [] (f : ια) :
Pairwise (Disjoint on f) ∀ ⦃m n : ι⦄, m < nDisjoint (f m) (f n)
theorem pairwise_disjoint_mono {α : Type u_1} {ι : Type u_4} {f : ια} {g : ια} [] [] (hs : Pairwise (Disjoint on f)) (h : g f) :
Pairwise (Disjoint on g)
theorem Set.Pairwise.mono {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (h : t s) (hs : s.Pairwise r) :
t.Pairwise r
theorem Set.Pairwise.mono' {α : Type u_1} {r : ααProp} {p : ααProp} {s : Set α} (H : r p) (hr : s.Pairwise r) :
s.Pairwise p
theorem Set.pairwise_top {α : Type u_1} (s : Set α) :
s.Pairwise
theorem Set.Subsingleton.pairwise {α : Type u_1} {s : Set α} (h : s.Subsingleton) (r : ααProp) :
s.Pairwise r
@[simp]
theorem Set.pairwise_empty {α : Type u_1} (r : ααProp) :
.Pairwise r
@[simp]
theorem Set.pairwise_singleton {α : Type u_1} (a : α) (r : ααProp) :
{a}.Pairwise r
theorem Set.pairwise_iff_of_refl {α : Type u_1} {r : ααProp} {s : Set α} [IsRefl α r] :
s.Pairwise r ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sr a b
theorem Set.Pairwise.of_refl {α : Type u_1} {r : ααProp} {s : Set α} [IsRefl α r] :
s.Pairwise r∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sr a b

Alias of the forward direction of Set.pairwise_iff_of_refl.

theorem Set.Nonempty.pairwise_iff_exists_forall {α : Type u_1} {ι : Type u_4} {r : ααProp} {f : ια} [IsEquiv α r] {s : Set ι} (hs : s.Nonempty) :
s.Pairwise (r on f) ∃ (z : α), xs, r (f x) z
theorem Set.Nonempty.pairwise_eq_iff_exists_eq {α : Type u_1} {ι : Type u_4} {s : Set α} (hs : s.Nonempty) {f : αι} :
(s.Pairwise fun (x y : α) => f x = f y) ∃ (z : ι), xs, f x = z

For a nonempty set s, a function f takes pairwise equal values on s if and only if for some z in the codomain, f takes value z on all x ∈ s. See also Set.pairwise_eq_iff_exists_eq for a version that assumes [Nonempty ι] instead of Set.Nonempty s.

theorem Set.pairwise_iff_exists_forall {α : Type u_1} {ι : Type u_4} [] (s : Set α) (f : αι) {r : ιιProp} [IsEquiv ι r] :
s.Pairwise (r on f) ∃ (z : ι), xs, r (f x) z
theorem Set.pairwise_eq_iff_exists_eq {α : Type u_1} {ι : Type u_4} [] (s : Set α) (f : αι) :
(s.Pairwise fun (x y : α) => f x = f y) ∃ (z : ι), xs, f x = z

A function f : α → ι with nonempty codomain takes pairwise equal values on a set s if and only if for some z in the codomain, f takes value z on all x ∈ s. See also Set.Nonempty.pairwise_eq_iff_exists_eq for a version that assumes Set.Nonempty s instead of [Nonempty ι].

theorem Set.pairwise_union {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} :
(s t).Pairwise r s.Pairwise r t.Pairwise r as, bt, a br a b r b a
theorem Set.pairwise_union_of_symmetric {α : Type u_1} {r : ααProp} {s : Set α} {t : Set α} (hr : ) :
(s t).Pairwise r s.Pairwise r t.Pairwise r as, bt, a br a b
theorem Set.pairwise_insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} :
(insert a s).Pairwise r s.Pairwise r bs, a br a b r b a
theorem Set.pairwise_insert_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (ha : as) :
(insert a s).Pairwise r s.Pairwise r bs, r a b r b a
theorem Set.Pairwise.insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : s.Pairwise r) (h : bs, a br a b r b a) :
(insert a s).Pairwise r
theorem Set.Pairwise.insert_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (ha : as) (hs : s.Pairwise r) (h : bs, r a b r b a) :
(insert a s).Pairwise r
theorem Set.pairwise_insert_of_symmetric {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hr : ) :
(insert a s).Pairwise r s.Pairwise r bs, a br a b
theorem Set.pairwise_insert_of_symmetric_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hr : ) (ha : as) :
(insert a s).Pairwise r s.Pairwise r bs, r a b
theorem Set.Pairwise.insert_of_symmetric {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : s.Pairwise r) (hr : ) (h : bs, a br a b) :
(insert a s).Pairwise r
theorem Set.Pairwise.insert_of_symmetric_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : s.Pairwise r) (hr : ) (ha : as) (h : bs, r a b) :
(insert a s).Pairwise r
theorem Set.pairwise_pair {α : Type u_1} {r : ααProp} {a : α} {b : α} :
{a, b}.Pairwise r a br a b r b a
theorem Set.pairwise_pair_of_symmetric {α : Type u_1} {r : ααProp} {a : α} {b : α} (hr : ) :
{a, b}.Pairwise r a br a b
theorem Set.pairwise_univ {α : Type u_1} {r : ααProp} :
Set.univ.Pairwise r
@[simp]
theorem Set.pairwise_bot_iff {α : Type u_1} {s : Set α} :
s.Pairwise s.Subsingleton
theorem Set.Pairwise.subsingleton {α : Type u_1} {s : Set α} :
s.Pairwise s.Subsingleton

Alias of the forward direction of Set.pairwise_bot_iff.

theorem Set.injOn_iff_pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ια} {s : Set ι} :
s.Pairwise fun (x x_1 : ι) => f x f x_1

See also Function.injective_iff_pairwise_ne

theorem Set.InjOn.pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ια} {s : Set ι} :
s.Pairwise fun (x x_1 : ι) => f x f x_1

Alias of the forward direction of Set.injOn_iff_pairwise_ne.

See also Function.injective_iff_pairwise_ne

theorem Set.Pairwise.image {α : Type u_1} {ι : Type u_4} {r : ααProp} {f : ια} {s : Set ι} (h : s.Pairwise (r on f)) :
(f '' s).Pairwise r
theorem Set.InjOn.pairwise_image {α : Type u_1} {ι : Type u_4} {r : ααProp} {f : ια} {s : Set ι} (h : ) :
(f '' s).Pairwise r s.Pairwise (r on f)

See also Set.Pairwise.image.

theorem Pairwise.range_pairwise {α : Type u_1} {ι : Type u_4} {r : ααProp} {f : ια} (hr : Pairwise (r on f)) :
().Pairwise r
theorem pairwise_subtype_iff_pairwise_set {α : Type u_1} (s : Set α) (r : ααProp) :
(Pairwise fun (x y : s) => r x y) s.Pairwise r
theorem Set.Pairwise.subtype {α : Type u_1} (s : Set α) (r : ααProp) :
s.Pairwise rPairwise fun (x y : s) => r x y

Alias of the reverse direction of pairwise_subtype_iff_pairwise_set.

theorem Pairwise.set_of_subtype {α : Type u_1} (s : Set α) (r : ααProp) :
(Pairwise fun (x y : s) => r x y)s.Pairwise r

Alias of the forward direction of pairwise_subtype_iff_pairwise_set.

def Set.PairwiseDisjoint {α : Type u_1} {ι : Type u_4} [] [] (s : Set ι) (f : ια) :

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.

Equations
• s.PairwiseDisjoint f = s.Pairwise (Disjoint on f)
Instances For
theorem Set.PairwiseDisjoint.subset {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {t : Set ι} {f : ια} (ht : t.PairwiseDisjoint f) (h : s t) :
s.PairwiseDisjoint f
theorem Set.PairwiseDisjoint.mono_on {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} {g : ια} (hs : s.PairwiseDisjoint f) (h : ∀ ⦃i : ι⦄, i sg i f i) :
s.PairwiseDisjoint g
theorem Set.PairwiseDisjoint.mono {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} {g : ια} (hs : s.PairwiseDisjoint f) (h : g f) :
s.PairwiseDisjoint g
@[simp]
theorem Set.pairwiseDisjoint_empty {α : Type u_1} {ι : Type u_4} [] [] {f : ια} :
.PairwiseDisjoint f
@[simp]
theorem Set.pairwiseDisjoint_singleton {α : Type u_1} {ι : Type u_4} [] [] (i : ι) (f : ια) :
{i}.PairwiseDisjoint f
theorem Set.pairwiseDisjoint_insert {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} {i : ι} :
(insert i s).PairwiseDisjoint f s.PairwiseDisjoint f js, i jDisjoint (f i) (f j)
theorem Set.pairwiseDisjoint_insert_of_not_mem {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} {i : ι} (hi : is) :
(insert i s).PairwiseDisjoint f s.PairwiseDisjoint f js, Disjoint (f i) (f j)
theorem Set.PairwiseDisjoint.insert {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} (hs : s.PairwiseDisjoint f) {i : ι} (h : js, i jDisjoint (f i) (f j)) :
(insert i s).PairwiseDisjoint f
theorem Set.PairwiseDisjoint.insert_of_not_mem {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} (hs : s.PairwiseDisjoint f) {i : ι} (hi : is) (h : js, Disjoint (f i) (f j)) :
(insert i s).PairwiseDisjoint f
theorem Set.PairwiseDisjoint.image_of_le {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} (hs : s.PairwiseDisjoint f) {g : ιι} (hg : f g f) :
(g '' s).PairwiseDisjoint f
theorem Set.InjOn.pairwiseDisjoint_image {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [] [] {f : ια} {g : ι'ι} {s : Set ι'} (h : ) :
(g '' s).PairwiseDisjoint f s.PairwiseDisjoint (f g)
theorem Set.PairwiseDisjoint.range {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} (g : sι) (hg : ∀ (i : s), f (g i) f i) (ht : s.PairwiseDisjoint f) :
().PairwiseDisjoint f
theorem Set.pairwiseDisjoint_union {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {t : Set ι} {f : ια} :
(s t).PairwiseDisjoint f s.PairwiseDisjoint f t.PairwiseDisjoint f ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j ti jDisjoint (f i) (f j)
theorem Set.PairwiseDisjoint.union {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {t : Set ι} {f : ια} (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint f) (h : ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j ti jDisjoint (f i) (f j)) :
(s t).PairwiseDisjoint f
theorem Set.PairwiseDisjoint.elim {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} (hs : s.PairwiseDisjoint f) {i : ι} {j : ι} (hi : i s) (hj : j s) (h : ¬Disjoint (f i) (f j)) :
i = j
theorem Set.PairwiseDisjoint.elim' {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} (hs : s.PairwiseDisjoint f) {i : ι} {j : ι} (hi : i s) (hj : j s) (h : f i f j ) :
i = j
theorem Set.PairwiseDisjoint.eq_of_le {α : Type u_1} {ι : Type u_4} [] [] {s : Set ι} {f : ια} (hs : s.PairwiseDisjoint f) {i : ι} {j : ι} (hi : i s) (hj : j s) (hf : f i ) (hij : f i f j) :
i = j

### Pairwise disjoint set of sets #

theorem Set.pairwiseDisjoint_range_singleton {ι : Type u_4} :
(Set.range singleton).PairwiseDisjoint id
theorem Set.pairwiseDisjoint_fiber {α : Type u_1} {ι : Type u_4} (f : ια) (s : Set α) :
s.PairwiseDisjoint fun (a : α) => f ⁻¹' {a}
theorem Set.PairwiseDisjoint.elim_set {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ιSet α} (hs : s.PairwiseDisjoint f) {i : ι} {j : ι} (hi : i s) (hj : j s) (a : α) (hai : a f i) (haj : a f j) :
i = j
theorem Set.PairwiseDisjoint.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} {ι' : Type u_5} {s : Set ι} {t : Set ι'} {f : ιSet α} {g : ι'Set β} (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint g) :
(s ×ˢ t).PairwiseDisjoint fun (i : ι × ι') => f i.1 ×ˢ g i.2
theorem Set.pairwiseDisjoint_pi {ι : Type u_4} {ι' : ιType u_6} {α : ιType u_7} {s : (i : ι) → Set (ι' i)} {f : (i : ι) → ι' iSet (α i)} (hs : ∀ (i : ι), (s i).PairwiseDisjoint (f i)) :
(Set.univ.pi s).PairwiseDisjoint fun (I : (i : ι) → ι' i) => Set.univ.pi fun (i : ι) => f i (I i)
theorem Set.pairwiseDisjoint_image_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {s : Set α} {t : Set β} (hf : as, Function.Injective (f a)) :
(s.PairwiseDisjoint fun (a : α) => f a '' t) Set.InjOn (fun (p : α × β) => f p.1 p.2) (s ×ˢ t)

The partial images of a binary function f whose partial evaluations are injective are pairwise disjoint iff f is injective .

theorem Set.pairwiseDisjoint_image_left_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {s : Set α} {t : Set β} (hf : bt, Function.Injective fun (a : α) => f a b) :
(t.PairwiseDisjoint fun (b : β) => (fun (a : α) => f a b) '' s) Set.InjOn (fun (p : α × β) => f p.1 p.2) (s ×ˢ t)

The partial images of a binary function f whose partial evaluations are injective are pairwise disjoint iff f is injective .

theorem Set.exists_ne_mem_inter_of_not_pairwiseDisjoint {α : Type u_1} {ι : Type u_4} {s : Set ι} {f : ιSet α} (h : ¬s.PairwiseDisjoint f) :
is, js, i j ∃ (x : α), x f i f j
theorem Set.exists_lt_mem_inter_of_not_pairwiseDisjoint {α : Type u_1} {ι : Type u_4} {s : Set ι} [] {f : ιSet α} (h : ¬s.PairwiseDisjoint f) :
is, js, i < j ∃ (x : α), x f i f j
theorem exists_ne_mem_inter_of_not_pairwise_disjoint {α : Type u_1} {ι : Type u_4} {f : ιSet α} (h : ¬Pairwise (Disjoint on f)) :
∃ (i : ι) (j : ι), i j ∃ (x : α), x f i f j
theorem exists_lt_mem_inter_of_not_pairwise_disjoint {α : Type u_1} {ι : Type u_4} [] {f : ιSet α} (h : ¬Pairwise (Disjoint on f)) :
∃ (i : ι) (j : ι), i < j ∃ (x : α), x f i f j
theorem pairwise_disjoint_fiber {α : Type u_1} {ι : Type u_4} (f : ια) :
Pairwise (Disjoint on fun (a : α) => f ⁻¹' {a})
theorem subsingleton_setOf_mem_iff_pairwise_disjoint {α : Type u_1} {ι : Type u_4} {f : ιSet α} :
(∀ (a : α), {i : ι | a f i}.Subsingleton) Pairwise (Disjoint on f)