mathlib documentation

data.set.pairwise

Relations holding pairwise #

This file defines pairwise relations and pairwise disjoint indexed sets.

Main declarations #

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

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

Equations
source
theorem pairwise.mono {α : Type u_1} {r p : α → α → Prop} (hr : pairwise r) (h : ∀ ⦃i j : α⦄, r i j → p i j) :
pairwise p
source
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
source
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
source
theorem symmetric.pairwise_on {α : Type u_1} {ι : Type u_2} {r : α → α → Prop} [linear_order ι] (hr : symmetric r) (f : ι → α) :
pairwise (r on f) ↔ ∀ (m n : ι), m < n → r (f m) (f n)
source
theorem pairwise_disjoint_on {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] [linear_order ι] (f : ι → α) :
pairwise (disjoint on f) ↔ ∀ (m n : ι), m < n → disjoint (f m) (f n)
source
@[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 ∈ s → x ≠ y → r x y
source
theorem set.pairwise_of_forall {α : Type u_1} (s : set α) (r : α → α → Prop) (h : ∀ (a b : α), r a b) :
s.pairwise r
source
theorem set.pairwise.imp_on {α : Type u_1} {r p : α → α → Prop} {s : set α} (h : s.pairwise r) (hrp : s.pairwise (λ ⦃a b : α⦄, r a b → p a b)) :
s.pairwise p
source
theorem set.pairwise.imp {α : Type u_1} {r p : α → α → Prop} {s : set α} (h : s.pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a b) :
s.pairwise p
source
theorem set.pairwise.mono {α : Type u_1} {r : α → α → Prop} {s t : set α} (h : t ⊆ s) (hs : s.pairwise r) :
t.pairwise r
source
theorem set.pairwise.mono' {α : Type u_1} {r p : α → α → Prop} {s : set α} (H : r ≤ p) (hr : s.pairwise r) :
s.pairwise p
source
theorem set.pairwise_top {α : Type u_1} (s : set α) :
s.pairwise ⊤
source
@[protected]
theorem set.subsingleton.pairwise {α : Type u_1} {s : set α} (h : s.subsingleton) (r : α → α → Prop) :
s.pairwise r
source
@[simp]
theorem set.pairwise_empty {α : Type u_1} (r : α → α → Prop) :
∅.pairwise r
source
@[simp]
theorem set.pairwise_singleton {α : Type u_1} (a : α) (r : α → α → Prop) :
{a}.pairwise r
source
theorem set.nonempty.pairwise_iff_exists_forall {α : Type u_1} {ι : Type u_2} {r : α → α → Prop} {f : ι → α} [is_equiv α r] {s : set ι} (hs : s.nonempty) :
s.pairwise (r on f) ↔ ∃ (z : α), ∀ (x : ι), x ∈ s → r (f x) z
source
theorem set.nonempty.pairwise_eq_iff_exists_eq {α : Type u_1} {ι : Type u_2} {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.

source
theorem set.pairwise_iff_exists_forall {α : Type u_1} {ι : Type u_2} [nonempty ι] (s : set α) (f : α → ι) {r : ι → ι → Prop} [is_equiv ι r] :
s.pairwise (r on f) ↔ ∃ (z : ι), ∀ (x : α), x ∈ s → r (f x) z
source
theorem set.pairwise_eq_iff_exists_eq {α : Type u_1} {ι : Type u_2} [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 ι].

source
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
source
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
source
theorem set.pairwise_insert {α : Type u_1} {r : α → α → Prop} {s : set α} {a : α} :
(insert a s).pairwise r ↔ s.pairwise r ∧ ∀ (b : α), b ∈ s → a ≠ b → r a b ∧ r b a
source
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 : α), b ∈ s → a ≠ b → r a b
source
theorem set.pairwise_pair {α : Type u_1} {r : α → α → Prop} {a b : α} :
{a, b}.pairwise r ↔ a ≠ b → r a b ∧ r b a
source
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
source
theorem set.pairwise_univ {α : Type u_1} {r : α → α → Prop} :
set.univ.pairwise r ↔ pairwise r
source
theorem set.pairwise.on_injective {α : Type u_1} {ι : Type u_2} {r : α → α → Prop} {f : ι → α} {s : set α} (hs : s.pairwise r) (hf : function.injective f) (hfs : ∀ (x : ι), f x ∈ s) :
pairwise (r on f)
source
theorem set.inj_on.pairwise_image {α : Type u_1} {ι : Type u_2} {r : α → α → Prop} {f : ι → α} {s : set ι} (h : set.inj_on f s) :
(f '' s).pairwise r ↔ s.pairwise (r on f)
source
theorem set.pairwise_Union {α : Type u_1} {ι : Type u_2} {r : α → α → Prop} {f : ι → set α} (h : directed has_subset.subset f) :
(⋃ (n : ι), f n).pairwise r ↔ ∀ (n : ι), (f n).pairwise r
source
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 ∈ s → a.pairwise r
source
theorem pairwise.set_pairwise {α : Type u_1} {r : α → α → Prop} (h : pairwise r) (s : set α) :
s.pairwise r
source
theorem pairwise_subtype_iff_pairwise_set {α : Type u_1} (s : set α) (r : α → α → Prop) :
pairwise (λ (x y : ↥s), r ↑x ↑y) ↔ s.pairwise r
source
theorem set.pairwise.subtype {α : Type u_1} (s : set α) (r : α → α → Prop) :
s.pairwise r → pairwise (λ (x y : ↥s), r ↑x ↑y)

Alias of pairwise_subtype_iff_pairwise_set.

source
theorem pairwise.set_of_subtype {α : Type u_1} (s : set α) (r : α → α → Prop) :
pairwise (λ (x y : ↥s), r ↑x ↑y) → s.pairwise r

Alias of pairwise_subtype_iff_pairwise_set.

source
def set.pairwise_disjoint {α : Type u_1} {ι : Type u_2} [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.

Equations
source
theorem set.pairwise_disjoint.subset {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {s t : set ι} {f : ι → α} (ht : t.pairwise_disjoint f) (h : s ⊆ t) :
s.pairwise_disjoint f
source
theorem set.pairwise_disjoint.mono_on {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {s : set ι} {f g : ι → α} (hs : s.pairwise_disjoint f) (h : ∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i) :
s.pairwise_disjoint g
source
theorem set.pairwise_disjoint.mono {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {s : set ι} {f g : ι → α} (hs : s.pairwise_disjoint f) (h : g ≤ f) :
s.pairwise_disjoint g
source
@[simp]
theorem set.pairwise_disjoint_empty {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {f : ι → α} :
∅.pairwise_disjoint f
source
@[simp]
theorem set.pairwise_disjoint_singleton {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] (i : ι) (f : ι → α) :
{i}.pairwise_disjoint f
source
theorem set.pairwise_disjoint_insert {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} {i : ι} :
(insert i s).pairwise_disjoint f ↔ s.pairwise_disjoint f ∧ ∀ (j : ι), j ∈ s → i ≠ j → disjoint (f i) (f j)
source
theorem set.pairwise_disjoint.insert {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {i : ι} (h : ∀ (j : ι), j ∈ s → i ≠ j → disjoint (f i) (f j)) :
(insert i s).pairwise_disjoint f
source
theorem set.pairwise_disjoint.image_of_le {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {s : set ι} {f : ι → α} (hs : s.pairwise_disjoint f) {g : ι → ι} (hg : f ∘ g ≤ f) :
(g '' s).pairwise_disjoint f
source
theorem set.inj_on.pairwise_disjoint_image {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [semilattice_inf α] [order_bot α] {f : ι → α} {g : ι' → ι} {s : set ι'} (h : set.inj_on g s) :
(g '' s).pairwise_disjoint f ↔ s.pairwise_disjoint (f ∘ g)
source
theorem set.pairwise_disjoint.range {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [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
source
theorem set.pairwise_disjoint_union {α : Type u_1} {ι : Type u_2} [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 ∈ t → i ≠ j → disjoint (f i) (f j)
source
theorem set.pairwise_disjoint.union {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [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
source
theorem set.pairwise_disjoint_Union {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [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
source
theorem set.pairwise_disjoint_sUnion {α : Type u_1} {ι : Type u_2} [semilattice_inf α] [order_bot α] {f : ι → α} {s : set (set ι)} (h : directed_on has_subset.subset s) :
(⋃₀s).pairwise_disjoint f ↔ ∀ ⦃a : set ι⦄, a ∈ s → a.pairwise_disjoint f
source
theorem set.pairwise_disjoint.elim {α : Type u_1} {ι : Type u_2} [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
source
theorem set.pairwise_disjoint.elim' {α : Type u_1} {ι : Type u_2} [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
source
theorem set.pairwise_disjoint.bUnion {α : Type u_1} {ι : Type u_2} {ι' : Type u_3} [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 #

source
theorem set.pairwise_disjoint_range_singleton {ι : Type u_2} :
(set.range singleton).pairwise_disjoint id
source
theorem set.pairwise_disjoint_fiber {α : Type u_1} {ι : Type u_2} (f : ι → α) (s : set α) :
s.pairwise_disjoint (λ (a : α), f ⁻¹' {a})
source
theorem set.pairwise_disjoint.elim_set {α : Type u_1} {ι : Type u_2} {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
source
theorem set.bUnion_diff_bUnion_eq {α : Type u_1} {ι : Type u_2} {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
source
noncomputable def set.bUnion_eq_sigma_of_disjoint {α : Type u_1} {ι : Type u_2} {s : set ι} {f : ι → set α} (h : s.pairwise (disjoint on f)) :
(↥⋃ (i : ι) (H : i ∈ s), f i) ≃ Σ (i : ↥s), ↥(f ↑i)

Equivalence between a disjoint bounded union and a dependent sum.

Equations
source
theorem pairwise_disjoint_fiber {α : Type u_1} {ι : Type u_2} (f : ι → α) :
pairwise (disjoint on λ (a : α), f ⁻¹' {a})