Documentation

Mathlib.Data.Set.Pairwise

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.Lattice 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 => bif c then a else b) r a b
theorem pairwise_disjoint_on_bool {α : Type u_1} [inst : ] [inst : ] {a : α} {b : α} :
Pairwise (Disjoint on fun c => bif c then a else b) Disjoint a b
theorem Symmetric.pairwise_on {α : Type u_2} {ι : Type u_1} {r : ααProp} [inst : ] (hr : ) (f : ια) :
Pairwise (r on f) m n : ι⦄ → m < nr (f m) (f n)
theorem pairwise_disjoint_on {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] [inst : ] (f : ια) :
Pairwise (Disjoint on f) ∀ ⦃m n : ι⦄, m < nDisjoint (f m) (f n)
theorem pairwise_disjoint_mono {α : Type u_1} {ι : Type u_2} {f : ια} {g : ια} [inst : ] [inst : ] (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 : ) :
theorem Set.Pairwise.mono' {α : Type u_1} {r : ααProp} {p : ααProp} {s : Set α} (H : r p) (hr : ) :
theorem Set.pairwise_top {α : Type u_1} (s : Set α) :
theorem Set.Subsingleton.pairwise {α : Type u_1} {s : Set α} (h : ) (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 α} [inst : IsRefl α r] :
a : α⦄ → a sb : α⦄ → b sr a b
theorem Set.Pairwise.of_refl {α : Type u_1} {r : ααProp} {s : Set α} [inst : IsRefl α r] :
a : α⦄ → a sb : α⦄ → 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_2} {r : ααProp} {f : ια} [inst : IsEquiv α r] {s : Set ι} (hs : ) :
Set.Pairwise s (r on f) z, (x : ι) → x sr (f x) z
theorem Set.Nonempty.pairwise_eq_iff_exists_eq {α : Type u_1} {ι : Type u_2} {s : Set α} (hs : ) {f : αι} :
(Set.Pairwise s fun 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∈ 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_2} {ι : Type u_1} [inst : ] (s : Set α) (f : αι) {r : ιιProp} [inst : IsEquiv ι r] :
Set.Pairwise s (r on f) z, (x : α) → x sr (f x) z
theorem Set.pairwise_eq_iff_exists_eq {α : Type u_2} {ι : Type u_1} [inst : ] (s : Set α) (f : αι) :
(Set.Pairwise s fun 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∈ 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 α} :
Set.Pairwise (s t) 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 : Set α} {t : Set α} (hr : ) :
Set.Pairwise (s t) r ((a : α) → a s(b : α) → b ta br a b)
theorem Set.pairwise_insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} :
Set.Pairwise (insert a s) r ∀ (b : α), b sa br a b r b a
theorem Set.pairwise_insert_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (ha : ¬a s) :
Set.Pairwise (insert a s) r ∀ (b : α), b sr a b r b a
theorem Set.Pairwise.insert {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : ) (h : ∀ (b : α), b sa br a b r b a) :
theorem Set.Pairwise.insert_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (ha : ¬a s) (hs : ) (h : ∀ (b : α), b sr a b r b a) :
theorem Set.pairwise_insert_of_symmetric {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hr : ) :
Set.Pairwise (insert a s) r ((b : α) → b sa br a b)
theorem Set.pairwise_insert_of_symmetric_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hr : ) (ha : ¬a s) :
Set.Pairwise (insert a s) r ((b : α) → b sr a b)
theorem Set.Pairwise.insert_of_symmetric {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : ) (hr : ) (h : (b : α) → b sa br a b) :
theorem Set.Pairwise.insert_of_symmetric_of_not_mem {α : Type u_1} {r : ααProp} {s : Set α} {a : α} (hs : ) (hr : ) (ha : ¬a s) (h : (b : α) → b sr a b) :
theorem Set.pairwise_pair {α : Type u_1} {r : ααProp} {a : α} {b : α} :
Set.Pairwise {a, b} r a br a b r b a
theorem Set.pairwise_pair_of_symmetric {α : Type u_1} {r : ααProp} {a : α} {b : α} (hr : ) :
Set.Pairwise {a, b} r a br a b
theorem Set.pairwise_univ {α : Type u_1} {r : ααProp} :
Set.Pairwise Set.univ r
@[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.InjOn.pairwise_image {α : Type u_2} {ι : Type u_1} {r : ααProp} {f : ια} {s : Set ι} (h : ) :
theorem Set.pairwise_unionᵢ {α : Type u_1} {ι : Type u_2} {r : ααProp} {f : ιSet α} (h : Directed (fun x x_1 => x x_1) f) :
Set.Pairwise (Set.unionᵢ fun n => f n) r ∀ (n : ι), Set.Pairwise (f n) r
theorem Set.pairwise_unionₛ {α : Type u_1} {r : ααProp} {s : Set (Set α)} (h : DirectedOn (fun x x_1 => x x_1) s) :
Set.Pairwise (⋃₀ s) r ∀ (a : Set α), a s
theorem pairwise_subtype_iff_pairwise_set {α : Type u_1} (s : Set α) (r : ααProp) :
(Pairwise fun x y => r x y)
theorem Set.Pairwise.subtype {α : Type u_1} (s : Set α) (r : ααProp) :
Pairwise fun x y => 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 => r x y) →

Alias of the forward direction of pairwise_subtype_iff_pairwise_set.

def Set.PairwiseDisjoint {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] (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
theorem Set.PairwiseDisjoint.subset {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {t : Set ι} {f : ια} (ht : ) (h : s t) :
theorem Set.PairwiseDisjoint.mono_on {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {f : ια} {g : ια} (hs : ) (h : ∀ ⦃i : ι⦄, i sg i f i) :
theorem Set.PairwiseDisjoint.mono {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {f : ια} {g : ια} (hs : ) (h : g f) :
@[simp]
theorem Set.pairwiseDisjoint_empty {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {f : ια} :
@[simp]
theorem Set.pairwiseDisjoint_singleton {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] (i : ι) (f : ια) :
theorem Set.pairwiseDisjoint_insert {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {f : ια} {i : ι} :
Set.PairwiseDisjoint (insert i s) f ∀ (j : ι), j si jDisjoint (f i) (f j)
theorem Set.pairwiseDisjoint_insert_of_not_mem {α : Type u_2} {ι : Type u_1} [inst : ] [inst : ] {s : Set ι} {f : ια} {i : ι} (hi : ¬i s) :
Set.PairwiseDisjoint (insert i s) f ∀ (j : ι), j sDisjoint (f i) (f j)
theorem Set.PairwiseDisjoint.insert {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {f : ια} (hs : ) {i : ι} (h : ∀ (j : ι), j si jDisjoint (f i) (f j)) :
theorem Set.PairwiseDisjoint.insert_of_not_mem {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {f : ια} (hs : ) {i : ι} (hi : ¬i s) (h : ∀ (j : ι), j sDisjoint (f i) (f j)) :
theorem Set.PairwiseDisjoint.image_of_le {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {f : ια} (hs : ) {g : ιι} (hg : f g f) :
theorem Set.InjOn.pairwiseDisjoint_image {α : Type u_3} {ι : Type u_2} {ι' : Type u_1} [inst : ] [inst : ] {f : ια} {g : ι'ι} {s : Set ι'} (h : ) :
theorem Set.PairwiseDisjoint.range {α : Type u_2} {ι : Type u_1} [inst : ] [inst : ] {s : Set ι} {f : ια} (g : sι) (hg : ∀ (i : s), f (g i) f i) (ht : ) :
theorem Set.pairwiseDisjoint_union {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {t : Set ι} {f : ια} :
Set.PairwiseDisjoint (s t) f ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j ti jDisjoint (f i) (f j)
theorem Set.PairwiseDisjoint.union {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {t : Set ι} {f : ια} (hs : ) (ht : ) (h : ∀ ⦃i : ι⦄, i s∀ ⦃j : ι⦄, j ti jDisjoint (f i) (f j)) :
theorem Set.pairwiseDisjoint_unionᵢ {α : Type u_3} {ι : Type u_1} {ι' : Type u_2} [inst : ] [inst : ] {f : ια} {g : ι'Set ι} (h : Directed (fun x x_1 => x x_1) g) :
Set.PairwiseDisjoint (Set.unionᵢ fun n => g n) f ∀ ⦃n : ι'⦄, Set.PairwiseDisjoint (g n) f
theorem Set.pairwiseDisjoint_unionₛ {α : Type u_2} {ι : Type u_1} [inst : ] [inst : ] {f : ια} {s : Set (Set ι)} (h : DirectedOn (fun x x_1 => x x_1) s) :
∀ ⦃a : Set ι⦄, a s
theorem Set.PairwiseDisjoint.elim {α : Type u_1} {ι : Type u_2} [inst : ] [inst : ] {s : Set ι} {f : ια} (hs : ) {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_2} [inst : ] [inst : ] {s : Set ι} {f : ια} (hs : ) {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_2} [inst : ] [inst : ] {s : Set ι} {f : ια} (hs : ) {i : ι} {j : ι} (hi : i s) (hj : j s) (hf : f i ) (hij : f i f j) :
i = j
theorem Set.PairwiseDisjoint.bunionᵢ {α : Type u_3} {ι : Type u_2} {ι' : Type u_1} [inst : ] {s : Set ι'} {g : ι'Set ι} {f : ια} (hs : Set.PairwiseDisjoint s fun i' => i, h, f i) (hg : ∀ (i : ι'), i sSet.PairwiseDisjoint (g i) f) :

Bind operation for Set.PairwiseDisjoint. If you want to only consider finsets of indices, you can use Set.PairwiseDisjoint.bunionᵢ_finset.

Pairwise disjoint set of sets #

theorem Set.pairwiseDisjoint_fiber {α : Type u_1} {ι : Type u_2} (f : ια) (s : Set α) :
Set.PairwiseDisjoint s fun a => f ⁻¹' {a}
theorem Set.PairwiseDisjoint.elim_set {α : Type u_2} {ι : Type u_1} {s : Set ι} {f : ιSet α} (hs : ) {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_2} {ι : Type u_1} {s : Set ι} {t : Set ι} {f : ιSet α} (h : Set.PairwiseDisjoint (s t) f) :
((Set.unionᵢ fun i => Set.unionᵢ fun h => f i) \ Set.unionᵢ fun i => Set.unionᵢ fun h => f i) = Set.unionᵢ fun i => Set.unionᵢ fun h => f i
noncomputable def Set.bunionᵢEqSigmaOfDisjoint {α : Type u_1} {ι : Type u_2} {s : Set ι} {f : ιSet α} (h : ) :
↑(Set.unionᵢ fun i => Set.unionᵢ fun h => f i) (i : s) × ↑(f i)

Equivalence between a disjoint bounded union and a dependent sum.

Equations
• One or more equations did not get rendered due to their size.
theorem Set.pairwiseDisjoint_image_right_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {s : Set α} {t : Set β} (hf : ∀ (a : α), a sFunction.Injective (f a)) :
(Set.PairwiseDisjoint s fun a => f a '' t) Set.InjOn (fun 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.pairwiseDisjoint_image_left_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : αβγ} {s : Set α} {t : Set β} (hf : ∀ (b : β), b tFunction.Injective fun a => f a b) :
(Set.PairwiseDisjoint t fun b => (fun a => f a b) '' s) Set.InjOn (fun 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_2} (f : ια) :
Pairwise (Disjoint on fun a => f ⁻¹' {a})
theorem Set.PairwiseDisjoint.subset_of_bunionᵢ_subset_bunionᵢ {α : Type u_1} {ι : Type u_2} {f : ιSet α} {s : Set ι} {t : Set ι} (h₀ : Set.PairwiseDisjoint (s t) f) (h₁ : ∀ (i : ι), i sSet.Nonempty (f i)) (h : (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) Set.unionᵢ fun i => Set.unionᵢ fun h => f i) :
s t
theorem Pairwise.subset_of_bunionᵢ_subset_bunionᵢ {α : Type u_2} {ι : Type u_1} {f : ιSet α} {s : Set ι} {t : Set ι} (h₀ : Pairwise (Disjoint on f)) (h₁ : ∀ (i : ι), i sSet.Nonempty (f i)) (h : (Set.unionᵢ fun i => Set.unionᵢ fun h => f i) Set.unionᵢ fun i => Set.unionᵢ fun h => f i) :
s t
theorem Pairwise.bunionᵢ_injective {α : Type u_2} {ι : Type u_1} {f : ιSet α} (h₀ : Pairwise (Disjoint on f)) (h₁ : ∀ (i : ι), Set.Nonempty (f i)) :
Function.Injective fun s => Set.unionᵢ fun i => Set.unionᵢ fun h => f i