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 : Symmetric r) {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} [SemilatticeInf α] [OrderBot α] {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} [LinearOrder ι] (hr : Symmetric r) (f : ι → α) : Pairwise (r on f) ↔ ∀ ⦃m n : ι⦄, m < n → r (f m) (f n)

theorem pairwise_disjoint_on {α : Type u_1} {ι : Type u_4} [SemilatticeInf α] [OrderBot α] [LinearOrder ι] (f : ι → α) : Pairwise (Disjoint on f) ↔ ∀ ⦃m n : ι⦄, m < n → Disjoint (f m) (f n)

theorem pairwise_disjoint_mono {α : Type u_1} {ι : Type u_4} {f : ι → α} {g : ι → α} [SemilatticeInf α] [OrderBot α] (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 ∈ s → r a b

theorem Set.Pairwise.of_refl {α : Type u_1} {r : α → α → Prop} {s : Set α} [IsRefl α r] : s.Pairwise r → ∀ ⦃a : α⦄, a ∈ s → ∀ ⦃b : α⦄, b ∈ s → r 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 : α), ∀ x ∈ s, 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 : ι), ∀ x ∈ s, 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} [Nonempty ι] (s : Set α) (f : α → ι) {r : ι → ι → Prop} [IsEquiv ι r] : s.Pairwise (r on f) ↔ ∃ (z : ι), ∀ x ∈ s, r (f x) z

theorem Set.pairwise_eq_iff_exists_eq {α : Type u_1} {ι : Type u_4} [Nonempty ι] (s : Set α) (f : α → ι) : (s.Pairwise fun (x y : α) => f x = f y) ↔ ∃ (z : ι), ∀ x ∈ s, 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 ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a

theorem Set.pairwise_union_of_symmetric {α : Type u_1} {r : α → α → Prop} {s : Set α} {t : Set α} (hr : Symmetric r) : (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b

theorem Set.pairwise_insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a

theorem Set.pairwise_insert_of_not_mem {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (ha : a ∉ s) : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a

theorem Set.Pairwise.insert {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hs : s.Pairwise r) (h : ∀ b ∈ s, a ≠ b → r 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 : a ∉ s) (hs : s.Pairwise r) (h : ∀ b ∈ s, 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 : Symmetric r) : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b

theorem Set.pairwise_insert_of_symmetric_of_not_mem {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hr : Symmetric r) (ha : a ∉ s) : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b

theorem Set.Pairwise.insert_of_symmetric {α : Type u_1} {r : α → α → Prop} {s : Set α} {a : α} (hs : s.Pairwise r) (hr : Symmetric r) (h : ∀ b ∈ s, a ≠ b → r 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 : Symmetric r) (ha : a ∉ s) (h : ∀ b ∈ s, r a b) : (insert a s).Pairwise r

theorem Set.pairwise_pair {α : Type u_1} {r : α → α → Prop} {a : α} {b : α} : {a, b}.Pairwise r ↔ a ≠ b → r a b ∧ r b a

theorem Set.pairwise_pair_of_symmetric {α : Type u_1} {r : α → α → Prop} {a : α} {b : α} (hr : Symmetric r) : {a, b}.Pairwise r ↔ a ≠ b → r a b

theorem Set.pairwise_univ {α : Type u_1} {r : α → α → Prop} : Set.univ.Pairwise r ↔ 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 ι} : Set.InjOn f s ↔ 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 ι} : Set.InjOn f s → 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 : Set.InjOn f s) : (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)) : (Set.range 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 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.

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

Alias of the reverse direction of pairwise_subtype_iff_pairwise_set.

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

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)

theorem Set.PairwiseDisjoint.subset {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {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} [PartialOrder α] [OrderBot α] {s : Set ι} {f : ι → α} {g : ι → α} (hs : s.PairwiseDisjoint f) (h : ∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i) : s.PairwiseDisjoint g

theorem Set.PairwiseDisjoint.mono {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {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} [PartialOrder α] [OrderBot α] {f : ι → α} : ∅.PairwiseDisjoint f

@[simp]

theorem Set.pairwiseDisjoint_singleton {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] (i : ι) (f : ι → α) : {i}.PairwiseDisjoint f

theorem Set.pairwiseDisjoint_insert {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {f : ι → α} {i : ι} : (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)

theorem Set.pairwiseDisjoint_insert_of_not_mem {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {f : ι → α} {i : ι} (hi : i ∉ s) : (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j)

theorem Set.PairwiseDisjoint.insert {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {f : ι → α} (hs : s.PairwiseDisjoint f) {i : ι} (h : ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)) : (insert i s).PairwiseDisjoint f

theorem Set.PairwiseDisjoint.insert_of_not_mem {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {f : ι → α} (hs : s.PairwiseDisjoint f) {i : ι} (hi : i ∉ s) (h : ∀ j ∈ s, Disjoint (f i) (f j)) : (insert i s).PairwiseDisjoint f

theorem Set.PairwiseDisjoint.image_of_le {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {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} [PartialOrder α] [OrderBot α] {f : ι → α} {g : ι' → ι} {s : Set ι'} (h : Set.InjOn g s) : (g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g)

theorem Set.PairwiseDisjoint.range {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {f : ι → α} (g : ↑s → ι) (hg : ∀ (i : ↑s), f (g i) ≤ f ↑i) (ht : s.PairwiseDisjoint f) : (Set.range g).PairwiseDisjoint f

theorem Set.pairwiseDisjoint_union {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {t : Set ι} {f : ι → α} : (s ∪ t).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ t.PairwiseDisjoint f ∧ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)

theorem Set.PairwiseDisjoint.union {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {t : Set ι} {f : ι → α} (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint f) (h : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)) : (s ∪ t).PairwiseDisjoint f

theorem Set.PairwiseDisjoint.elim {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {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.eq_or_disjoint {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {s : Set ι} {f : ι → α} (h : s.PairwiseDisjoint f) {i : ι} {j : ι} (hi : i ∈ s) (hj : j ∈ s) : i = j ∨ Disjoint (f i) (f j)

theorem Set.pairwiseDisjoint_range_iff {α : Type u_6} {β : Type u_7} {f : α → Set β} : (Set.range f).PairwiseDisjoint id ↔ ∀ (x y : α), f x = f y ∨ Disjoint (f x) (f y)

theorem Pairwise.pairwiseDisjoint {α : Type u_1} {ι : Type u_4} [PartialOrder α] [OrderBot α] {f : ι → α} (h : Pairwise (Disjoint on f)) (s : Set ι) : s.PairwiseDisjoint f

If the range of f is pairwise disjoint, then the image of any set s under f is as well.

theorem Set.PairwiseDisjoint.elim' {α : Type u_1} {ι : Type u_4} [SemilatticeInf α] [OrderBot α] {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} [SemilatticeInf α] [OrderBot α] {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 : ι) → ι' i → Set (α 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 : ∀ a ∈ s, 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 : ∀ b ∈ t, 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) : ∃ i ∈ s, ∃ j ∈ s, 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 ι} [LinearOrder ι] {f : ι → Set α} (h : ¬s.PairwiseDisjoint f) : ∃ i ∈ s, ∃ j ∈ s, 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} [LinearOrder ι] {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)