mathlib documentation

data.set.pairwise

Relations holding pairwise #

This file defines pairwise relations and pairwise disjoint indexed sets.

Main declarations #

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.

def pairwise {α : Type u_1} (r : α → α → Prop) :
Prop

A relation r holds pairwise if r i j for all i ≠ j.

Equations
theorem pairwise.mono {α : Type u_1} {r p : α → α → Prop} (hr : pairwise r) (h : ∀ ⦃i j : α⦄, r i jp i j) :
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 < nr (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 < ndisjoint (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) :
theorem function.injective_iff_pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ι → α} :
theorem function.injective.pairwise_ne {α : Type u_1} {ι : Type u_4} {f : ι → α} :

Alias of the forward direction of function.injective_iff_pairwise_ne`.

@[protected]
def set.pairwise {α : Type u_1} (s : set α) (r : α → α → Prop) :
Prop

The relation r holds pairwise on the set s if r x y for all distinct x y ∈ s.

Equations
  • s.pairwise r = ∀ ⦃x : α⦄, x s∀ ⦃y : α⦄, y sx yr x y
Instances for set.pairwise
theorem set.pairwise_of_forall {α : Type u_1} (s : set α) (r : α → α → Prop) (h : ∀ (a b : α), r a b) :
theorem set.pairwise.imp_on {α : Type u_1} {r p : α → α → Prop} {s : set α} (h : s.pairwise r) (hrp : s.pairwise (λ ⦃a b : α⦄, r a bp a b)) :
theorem set.pairwise.imp {α : Type u_1} {r p : α → α → Prop} {s : set α} (h : s.pairwise r) (hpq : ∀ ⦃a b : α⦄, r a bp a b) :
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) :
@[protected]
theorem set.pairwise.eq {α : Type u_1} {r : α → α → Prop} {s : set α} {a b : α} (hs : s.pairwise r) (ha : a s) (hb : b s) (h : ¬r a b) :
a = b
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) :
{a}.pairwise r
theorem set.pairwise_iff_of_refl {α : Type u_1} {r : α → α → Prop} {s : set α} [is_refl α r] :
s.pairwise r ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sr 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 sr a b

Alias of the forward direction of set.pairwise_iff_of_refl`.

theorem reflexive.set_pairwise_iff {α : Type u_1} {r : α → α → Prop} {s : set α} (hr : reflexive r) :
s.pairwise r ∀ ⦃a : α⦄, a s∀ ⦃b : α⦄, b sr a b
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 sr (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 sf 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 sr (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 sf 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 ta br 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 ta br 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 sa br a b r b a
theorem set.pairwise.insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} (hs : s.pairwise r) (h : ∀ (b : α), b sa br a b r b a) :
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 sa br 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 sa br a b) :
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 : symmetric r) :
{a, b}.pairwise r a br a b
theorem set.pairwise_univ {α : Type u_1} {r : α → α → Prop} :
@[simp]
theorem set.pairwise_bot_iff {α : Type u_1} {s : set α} :
theorem set.pairwise.subsingleton {α : Type u_1} {s : set α} :

Alias of the forward direction of set.pairwise_bot_iff`.

theorem set.pairwise.on_injective {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} {s : set α} (hs : s.pairwise r) (hf : function.injective f) (hfs : ∀ (x : ι), f x s) :
pairwise (r on f)
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 set.pairwise_Union {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → set α} (h : directed has_subset.subset f) :
(⋃ (n : ι), f n).pairwise r ∀ (n : ι), (f n).pairwise r
theorem set.pairwise_sUnion {α : Type u_1} {r : α → α → Prop} {s : set (set α)} (h : directed_on has_subset.subset s) :
(⋃₀ s).pairwise r ∀ (a : set α), a sa.pairwise r
theorem pairwise.set_pairwise {α : Type u_1} {r : α → α → Prop} (h : pairwise r) (s : set α) :
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 rpairwise (λ (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} [semilattice_inf α] [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
theorem set.pairwise_disjoint.subset {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s t : set ι} {f : ι → α} (ht : t.pairwise_disjoint f) (h : s t) :
theorem set.pairwise_disjoint.mono_on {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f g : ι → α} (hs : s.pairwise_disjoint f) (h : ∀ ⦃i : ι⦄, i sg i f i) :
theorem set.pairwise_disjoint.mono {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f g : ι → α} (hs : s.pairwise_disjoint f) (h : g f) :
@[simp]
theorem set.pairwise_disjoint_empty {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {f : ι → α} :
@[simp]
theorem set.pairwise_disjoint_singleton {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] (i : ι) (f : ι → α) :
theorem set.pairwise_disjoint_insert {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} {i : ι} :
(has_insert.insert i s).pairwise_disjoint f s.pairwise_disjoint f ∀ (j : ι), j si jdisjoint (f i) (f j)
theorem set.pairwise_disjoint.insert {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {i : ι} (h : ∀ (j : ι), j si jdisjoint (f i) (f j)) :
theorem set.pairwise_disjoint.image_of_le {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {g : ι → ι} (hg : f g f) :
theorem set.inj_on.pairwise_disjoint_image {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [semilattice_inf α] [order_bot α] {f : ι → α} {g : ι' → ι} {s : set ι'} (h : set.inj_on g s) :
theorem set.pairwise_disjoint.range {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} (g : s → ι) (hg : ∀ (i : s), f (g i) f i) (ht : s.pairwise_disjoint f) :
theorem set.pairwise_disjoint_union {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s t : set ι} {f : ι → α} :
(s t).pairwise_disjoint f s.pairwise_disjoint f t.pairwise_disjoint f ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j ti jdisjoint (f i) (f j)
theorem set.pairwise_disjoint.union {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {s t : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) (ht : t.pairwise_disjoint f) (h : ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j ti jdisjoint (f i) (f j)) :
theorem set.pairwise_disjoint_Union {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [semilattice_inf α] [order_bot α] {f : ι → α} {g : ι' → set ι} (h : directed has_subset.subset g) :
(⋃ (n : ι'), g n).pairwise_disjoint f ∀ ⦃n : ι'⦄, (g n).pairwise_disjoint f
theorem set.pairwise_disjoint_sUnion {α : Type u_1} {ι : Type u_4} [semilattice_inf α] [order_bot α] {f : ι → α} {s : set (set ι)} (h : directed_on has_subset.subset s) :
(⋃₀ s).pairwise_disjoint f ∀ ⦃a : set ι⦄, a sa.pairwise_disjoint f
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 : ¬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
theorem set.pairwise_disjoint.bUnion {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [complete_lattice α] {s : set ι'} {g : ι' → set ι} {f : ι → α} (hs : s.pairwise_disjoint (λ (i' : ι'), ⨆ (i : ι) (H : i g i'), f i)) (hg : ∀ (i : ι'), i s(g i).pairwise_disjoint f) :
(⋃ (i : ι') (H : i s), g i).pairwise_disjoint f

Bind operation for set.pairwise_disjoint. If you want to only consider finsets of indices, you can use set.pairwise_disjoint.bUnion_finset.

Pairwise disjoint set of sets #

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.bUnion_diff_bUnion_eq {α : Type u_1} {ι : Type u_4} {s t : set ι} {f : ι → set α} (h : (s t).pairwise_disjoint f) :
((⋃ (i : ι) (H : i s), f i) \ ⋃ (i : ι) (H : i t), f i) = ⋃ (i : ι) (H : i s \ t), f i
noncomputable def set.bUnion_eq_sigma_of_disjoint {α : Type u_1} {ι : Type u_4} {s : set ι} {f : ι → set α} (h : s.pairwise_disjoint f) :
(⋃ (i : ι) (H : i s), f i) Σ (i : s), (f i)

Equivalence between a disjoint bounded union and a dependent sum.

Equations
theorem set.pairwise_disjoint_image_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β → γ} {s : set α} {t : set β} (hf : ∀ (a : α), a sfunction.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 tfunction.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})