mathlib3 documentation

data.set.pairwise.basic

Relations holding pairwise #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.pairwise_disjoint: s.pairwise_disjoint f states that images under f of distinct elements of s are either equal or disjoint.

Notes #

The spelling s.pairwise_disjoint id is preferred over s.pairwise disjoint to permit dot notation on set.pairwise_disjoint, 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 λ (c : bool), cond c a b) ↔ r a b

theorem pairwise_disjoint_on_bool {α : Type u_1} [semilattice_inf α] [order_bot α] {a b : α} :

pairwise (disjoint on λ (c : bool), cond c a b) ↔ disjoint a b

theorem symmetric.pairwise_on {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} [linear_order ι] (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} [semilattice_inf α] [order_bot α] [linear_order ι] (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 : ι → α} [semilattice_inf α] [order_bot α] (hs : pairwise (disjoint on f)) (h : g ≤ f) :

pairwise (disjoint on g)

theorem set.pairwise.mono {α : Type u_1} {r : α → α → Prop} {s t : set α} (h : t ⊆ s) (hs : s.pairwise r) :

theorem set.pairwise.mono' {α : Type u_1} {r p : α → α → Prop} {s : set α} (H : r ≤ p) (hr : s.pairwise r) :

theorem set.pairwise_top {α : Type u_1} (s : set α) :

@[protected]

theorem set.subsingleton.pairwise {α : Type u_1} {s : set α} (h : s.subsingleton) (r : α → α → Prop) :

@[simp]

theorem set.pairwise_empty {α : Type u_1} (r : α → α → Prop) :

@[simp]

theorem set.pairwise_singleton {α : Type u_1} (a : α) (r : α → α → Prop) :

theorem set.pairwise_iff_of_refl {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α 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 α} [is_refl α 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 : ι → α} [is_equiv α r] {s : set ι} (hs : s.nonempty) :

s.pairwise (r on f) ↔ ∃ (z : α), ∀ (x : ι), 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 (λ (x y : α), f x = f y) ↔ ∃ (z : ι), ∀ (x : α), 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} [is_equiv ι r] :

s.pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), 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 (λ (x y : α), f x = f y) ↔ ∃ (z : ι), ∀ (x : α), 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 t : set α} :

(s ∪ t).pairwise r ↔ s.pairwise r ∧ t.pairwise r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b ∧ r b a

theorem set.pairwise_union_of_symmetric {α : Type u_1} {r : α → α → Prop} {s t : set α} (hr : symmetric r) :

(s ∪ t).pairwise r ↔ s.pairwise r ∧ t.pairwise r ∧ ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → a ≠ b → r a b

theorem set.pairwise_insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} :

(has_insert.insert a s).pairwise r ↔ s.pairwise r ∧ ∀ (b : α), 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) :

(has_insert.insert a s).pairwise r ↔ s.pairwise r ∧ ∀ (b : α), 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 : α), b ∈ s → a ≠ b → r a b ∧ r b a) :

(has_insert.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 : α), b ∈ s → r a b ∧ r b a) :

(has_insert.insert a s).pairwise r

theorem set.pairwise_insert_of_symmetric {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hr : symmetric r) :

(has_insert.insert a s).pairwise r ↔ s.pairwise r ∧ ∀ (b : α), 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) :

(has_insert.insert a s).pairwise r ↔ s.pairwise r ∧ ∀ (b : α), 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 : α), b ∈ s → a ≠ b → r a b) :

(has_insert.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 : α), b ∈ s → r a b) :

(has_insert.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.inj_on.pairwise_image {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} {s : set ι} (h : set.inj_on f s) :

(f '' s).pairwise r ↔ s.pairwise (r on f)

theorem pairwise_subtype_iff_pairwise_set {α : Type u_1} (s : set α) (r : α → α → Prop) :

pairwise (λ (x y : ↥s), r ↑x ↑y) ↔ s.pairwise r

theorem set.pairwise.subtype {α : Type u_1} (s : set α) (r : α → α → Prop) :

s.pairwise r → pairwise (λ (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 (λ (x y : ↥s), r ↑x ↑y) → s.pairwise r

Alias of the forward direction of pairwise_subtype_iff_pairwise_set.

def set.pairwise_disjoint {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] (s : set ι) (f : ι → α) :

Prop

A set is pairwise_disjoint under f, if the images of any distinct two elements under f are disjoint.

s.pairwise disjoint is (definitionally) the same as s.pairwise_disjoint id. We prefer the latter in order to allow dot notation on set.pairwise_disjoint, even though the former unfolds more nicely.

Equations

s.pairwise_disjoint f = s.pairwise (disjoint on f)

theorem set.pairwise_disjoint.subset {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s t : set ι} {f : ι → α} (ht : t.pairwise_disjoint f) (h : s ⊆ t) :

s.pairwise_disjoint f

theorem set.pairwise_disjoint.mono_on {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f g : ι → α} (hs : s.pairwise_disjoint f) (h : ∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i) :

s.pairwise_disjoint g

theorem set.pairwise_disjoint.mono {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f g : ι → α} (hs : s.pairwise_disjoint f) (h : g ≤ f) :

s.pairwise_disjoint g

@[simp]

theorem set.pairwise_disjoint_empty {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {f : ι → α} :

∅.pairwise_disjoint f

@[simp]

theorem set.pairwise_disjoint_singleton {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] (i : ι) (f : ι → α) :

{i}.pairwise_disjoint f

theorem set.pairwise_disjoint_insert {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f : ι → α} {i : ι} :

(has_insert.insert i s).pairwise_disjoint f ↔ s.pairwise_disjoint f ∧ ∀ (j : ι), j ∈ s → i ≠ j → disjoint (f i) (f j)

theorem set.pairwise_disjoint_insert_of_not_mem {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f : ι → α} {i : ι} (hi : i ∉ s) :

(has_insert.insert i s).pairwise_disjoint f ↔ s.pairwise_disjoint f ∧ ∀ (j : ι), j ∈ s → disjoint (f i) (f j)

theorem set.pairwise_disjoint.insert {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {i : ι} (h : ∀ (j : ι), j ∈ s → i ≠ j → disjoint (f i) (f j)) :

(has_insert.insert i s).pairwise_disjoint f

theorem set.pairwise_disjoint.insert_of_not_mem {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {i : ι} (hi : i ∉ s) (h : ∀ (j : ι), j ∈ s → disjoint (f i) (f j)) :

(has_insert.insert i s).pairwise_disjoint f

theorem set.pairwise_disjoint.image_of_le {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {g : ι → ι} (hg : f ∘ g ≤ f) :

(g '' s).pairwise_disjoint f

theorem set.inj_on.pairwise_disjoint_image {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [partial_order α] [order_bot α] {f : ι → α} {g : ι' → ι} {s : set ι'} (h : set.inj_on g s) :

(g '' s).pairwise_disjoint f ↔ s.pairwise_disjoint (f ∘ g)

theorem set.pairwise_disjoint.range {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f : ι → α} (g : ↥s → ι) (hg : ∀ (i : ↥s), f (g i) ≤ f ↑i) (ht : s.pairwise_disjoint f) :

(set.range g).pairwise_disjoint f

theorem set.pairwise_disjoint_union {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s t : set ι} {f : ι → α} :

(s ∪ t).pairwise_disjoint f ↔ s.pairwise_disjoint f ∧ t.pairwise_disjoint f ∧ ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → disjoint (f i) (f j)

theorem set.pairwise_disjoint.union {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s t : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) (ht : t.pairwise_disjoint f) (h : ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ t → i ≠ j → disjoint (f i) (f j)) :

(s ∪ t).pairwise_disjoint f

theorem set.pairwise_disjoint.elim {α : Type u_1} {ι : Type u_4} [partial_order α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (h : ¬disjoint (f i) (f j)) :

i = j

theorem set.pairwise_disjoint.elim' {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (h : f i ⊓ f j ≠ ⊥) :

i = j

theorem set.pairwise_disjoint.eq_of_le {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint 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.pairwise_disjoint_range_singleton {ι : Type u_4} :

(set.range has_singleton.singleton).pairwise_disjoint id

theorem set.pairwise_disjoint_fiber {α : Type u_1} {ι : Type u_4} (f : ι → α) (s : set α) :

s.pairwise_disjoint (λ (a : α), f ⁻¹' {a})

theorem set.pairwise_disjoint.elim_set {α : Type u_1} {ι : Type u_4} {s : set ι} {f : ι → set α} (hs : s.pairwise_disjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (a : α) (hai : a ∈ f i) (haj : a ∈ f j) :

i = j

theorem set.pairwise_disjoint.prod {α : Type u_1} {β : Type u_2} {ι : Type u_4} {ι' : Type u_5} {s : set ι} {t : set ι'} {f : ι → set α} {g : ι' → set β} (hs : s.pairwise_disjoint f) (ht : t.pairwise_disjoint g) :

(s ×ˢ t).pairwise_disjoint (λ (i : ι × ι'), f i.fst ×ˢ g i.snd)

theorem set.pairwise_disjoint_pi {ι : Type u_4} {ι' : ι → Type u_1} {α : ι → Type u_2} {s : Π (i : ι), set (ι' i)} {f : Π (i : ι), ι' i → set (α i)} (hs : ∀ (i : ι), (s i).pairwise_disjoint (f i)) :

(set.univ.pi s).pairwise_disjoint (λ (I : Π (i : ι), ι' i), set.univ.pi (λ (i : ι), f i (I i)))

theorem set.pairwise_disjoint_image_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} (hf : ∀ (a : α), a ∈ s → function.injective (f a)) :

s.pairwise_disjoint (λ (a : α), f a '' t) ↔ set.inj_on (λ (p : α × β), f p.fst p.snd) (s ×ˢ t)

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

theorem set.pairwise_disjoint_image_left_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} (hf : ∀ (b : β), b ∈ t → function.injective (λ (a : α), f a b)) :

t.pairwise_disjoint (λ (b : β), (λ (a : α), f a b) '' s) ↔ set.inj_on (λ (p : α × β), f p.fst p.snd) (s ×ˢ t)

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

theorem pairwise_disjoint_fiber {α : Type u_1} {ι : Type u_4} (f : ι → α) :

pairwise (disjoint on λ (a : α), f ⁻¹' {a})