Mathlib.Data.Set.Pairwise.Basic

pairwise_on_bool theorem

(hr : Symmetric r) {a b : α} : Pairwise (r on fun c => cond c a b) ↔ r a b

Full source

theorem pairwise_on_bool (hr : Symmetric r) {a b : α} :
    PairwisePairwise (r on fun c => cond c a b) ↔ r a b := by simpa [Pairwise, Function.onFun] using @hr a b

Pairwise Relation on Boolean Case Distinction ↔ Relation Between Elements

Informal description

Given a symmetric relation $r$ on a type $\alpha$ and two elements $a, b \in \alpha$, the relation $r$ holds pairwise on the function $f(c) = \text{cond}(c, a, b)$ (which maps `true` to $a$ and `false` to $b$) if and only if $r(a, b)$ holds. In other words, the pairwise relation on the boolean case distinction function is equivalent to the relation between the two distinguished elements.

pairwise_disjoint_on_bool theorem

[PartialOrder α] [OrderBot α] {a b : α} : Pairwise (Disjoint on fun c => cond c a b) ↔ Disjoint a b

Full source

theorem pairwise_disjoint_on_bool [PartialOrder α] [OrderBot α] {a b : α} :
    PairwisePairwise (Disjoint on fun c => cond c a b) ↔ Disjoint a b :=
  pairwise_on_bool Disjoint.symm

Pairwise Disjointness of Boolean Case Distinction ↔ Disjointness of Elements

Informal description

Let $\alpha$ be a partially ordered set with a least element $\bot$. For any two elements $a, b \in \alpha$, the images of the function $f(c) = \text{cond}(c, a, b)$ (which maps `true` to $a$ and `false` to $b$) are pairwise disjoint if and only if $a$ and $b$ are disjoint, i.e., $a \sqcap b = \bot$.

Symmetric.pairwise_on theorem

[LinearOrder ι] (hr : Symmetric r) (f : ι → α) : Pairwise (r on f) ↔ ∀ ⦃m n⦄, m < n → r (f m) (f n)

Full source

theorem Symmetric.pairwise_on [LinearOrder ι] (hr : Symmetric r) (f : ι → α) :
    PairwisePairwise (r on f) ↔ ∀ ⦃m n⦄, m < n → r (f m) (f n) :=
  ⟨fun h _m _n hmn => h hmn.ne, fun h _m _n hmn => hmn.lt_or_lt.elim (@h _ _) fun h' => hr (h h')⟩

Symmetric Pairwise Relation on Linearly Ordered Domain ↔ Relation Holds for All Ordered Pairs

Informal description

Let $\iota$ be a linearly ordered type, $\alpha$ an arbitrary type, and $r$ a symmetric relation on $\alpha$. For any function $f \colon \iota \to \alpha$, the relation $r$ holds pairwise on $f$ (i.e., $r(f(i), f(j))$ for all distinct $i,j \in \iota$) if and only if for any two indices $m < n$ in $\iota$, the relation $r(f(m), f(n))$ holds.

pairwise_disjoint_on theorem

 [PartialOrder α] [OrderBot α] [LinearOrder ι] (f : ι → α) :
  Pairwise (Disjoint on f) ↔ ∀ ⦃m n⦄, m < n → Disjoint (f m) (f n)

Full source

theorem pairwise_disjoint_on [PartialOrder α] [OrderBot α] [LinearOrder ι] (f : ι → α) :
    PairwisePairwise (Disjoint on f) ↔ ∀ ⦃m n⦄, m < n → Disjoint (f m) (f n) :=
  Symmetric.pairwise_on Disjoint.symm f

Pairwise Disjointness on Linearly Ordered Domain ↔ Disjointness for Ordered Pairs

Informal description

Let $\alpha$ be a partially ordered set with a least element $\bot$, and let $\iota$ be a linearly ordered set. For any function $f \colon \iota \to \alpha$, the images of $f$ are pairwise disjoint (i.e., for all distinct $i, j \in \iota$, $f(i) \sqcap f(j) = \bot$) if and only if for any two indices $m < n$ in $\iota$, the elements $f(m)$ and $f(n)$ are disjoint.

pairwise_disjoint_mono theorem

[PartialOrder α] [OrderBot α] (hs : Pairwise (Disjoint on f)) (h : g ≤ f) : Pairwise (Disjoint on g)

Full source

theorem pairwise_disjoint_mono [PartialOrder α] [OrderBot α] (hs : Pairwise (DisjointDisjoint on f))
    (h : g ≤ f) : Pairwise (DisjointDisjoint on g) :=
  hs.mono fun i j hij => Disjoint.mono (h i) (h j) hij

Monotonicity of Pairwise Disjointness under Function Comparison

Informal description

Let $\alpha$ be a partially ordered set with a least element $\bot$. Given two functions $f, g \colon \iota \to \alpha$ such that $g \leq f$ (i.e., $g(i) \leq f(i)$ for all $i \in \iota$), if the images of $f$ are pairwise disjoint, then the images of $g$ are also pairwise disjoint.

Pairwise.disjoint_extend_bot theorem

 [PartialOrder γ] [OrderBot γ] {e : α → β} {f : α → γ} (hf : Pairwise (Disjoint on f)) (he : FactorsThrough f e) :
  Pairwise (Disjoint on extend e f ⊥)

Full source

theorem Pairwise.disjoint_extend_bot [PartialOrder γ] [OrderBot γ]
    {e : α → β} {f : α → γ} (hf : Pairwise (DisjointDisjoint on f)) (he : FactorsThrough f e) :
    Pairwise (DisjointDisjoint on extend e f ⊥) := by
  intro b₁ b₂ hne
  rcases em (∃ a₁, e a₁ = b₁) with ⟨a₁, rfl⟩ | hb₁
  · rcases em (∃ a₂, e a₂ = b₂) with ⟨a₂, rfl⟩ | hb₂
    · simpa only [onFun, he.extend_apply] using hf (ne_of_apply_ne e hne)
    · simpa only [onFun, extend_apply' _ _ _ hb₂] using disjoint_bot_right
  · simpa only [onFun, extend_apply' _ _ _ hb₁] using disjoint_bot_left

Pairwise Disjointness Preservation under Function Extension with Bottom Default

Informal description

Let $\gamma$ be a partially ordered set with a least element $\bot$, and let $e : \alpha \to \beta$ and $f : \alpha \to \gamma$ be functions. If the images of $f$ are pairwise disjoint (i.e., for any distinct $i, j \in \alpha$, $f(i) \sqcap f(j) = \bot$) and $e$ factors through $f$, then the images of the extended function $\text{extend}\,e\,f\,\bot : \beta \to \gamma$ are also pairwise disjoint.

Set.Pairwise.mono theorem

(h : t ⊆ s) (hs : s.Pairwise r) : t.Pairwise r

Full source

theorem Pairwise.mono (h : t ⊆ s) (hs : s.Pairwise r) : t.Pairwise r :=
  fun _x xt _y yt => hs (h xt) (h yt)

Pairwise Relation Preservation under Subset Inclusion

Informal description

Let $s$ and $t$ be sets in a type $\alpha$, and let $r$ be a binary relation on $\alpha$. If $t$ is a subset of $s$ ($t \subseteq s$) and the relation $r$ holds pairwise for all distinct elements in $s$ ($s.\text{Pairwise}\, r$), then $r$ also holds pairwise for all distinct elements in $t$ ($t.\text{Pairwise}\, r$).

Set.Pairwise.mono' theorem

(H : r ≤ p) (hr : s.Pairwise r) : s.Pairwise p

Full source

theorem Pairwise.mono' (H : r ≤ p) (hr : s.Pairwise r) : s.Pairwise p :=
  hr.imp H

Monotonicity of Pairwise Relations: Weaker Relation Implies Stronger Pairwise Property

Informal description

Let $r$ and $p$ be binary relations on a type $\alpha$, and let $s$ be a set of elements of $\alpha$. If $r$ implies $p$ (i.e., $r(x,y) \to p(x,y)$ for all $x,y \in \alpha$) and $s$ is pairwise $r$-related, then $s$ is also pairwise $p$-related.

Set.pairwise_top theorem

(s : Set α) : s.Pairwise ⊤

Full source

theorem pairwise_top (s : Set α) : s.Pairwise ⊤ :=
  pairwise_of_forall s _ fun _ _ => trivial

Trivial Pairwise Relation on Any Set

Informal description

For any set $s$ in a type $\alpha$, the trivial relation $\top$ (which always holds) is pairwise satisfied on $s$. That is, for any two distinct elements $x, y \in s$, the relation $\top(x, y)$ holds.

Set.Subsingleton.pairwise theorem

(h : s.Subsingleton) (r : α → α → Prop) : s.Pairwise r

Full source

protected theorem Subsingleton.pairwise (h : s.Subsingleton) (r : α → α → Prop) : s.Pairwise r :=
  fun _x hx _y hy hne => (hne (h hx hy)).elim

Pairwise Relation Holds on Subsingleton Sets

Informal description

For any set $s$ that is a subsingleton (i.e., has at most one element) and any binary relation $r$ on elements of $s$, the relation $r$ holds pairwise on $s$.

Set.pairwise_empty theorem

(r : α → α → Prop) : (∅ : Set α).Pairwise r

Full source

@[simp]
theorem pairwise_empty (r : α → α → Prop) : (∅ : Set α).Pairwise r :=
  subsingleton_empty.pairwise r

Empty Set Satisfies Any Pairwise Relation

Informal description

For any binary relation $r$ on a type $\alpha$, the empty set $\emptyset \subseteq \alpha$ satisfies the pairwise relation with respect to $r$.

Set.pairwise_singleton theorem

(a : α) (r : α → α → Prop) : Set.Pairwise { a } r

Full source

@[simp]
theorem pairwise_singleton (a : α) (r : α → α → Prop) : Set.Pairwise {a} r :=
  subsingleton_singleton.pairwise r

Singleton Sets Satisfy Any Pairwise Relation

Informal description

For any element $a$ of type $\alpha$ and any binary relation $r$ on $\alpha$, the singleton set $\{a\}$ satisfies the pairwise relation $r$.

Set.pairwise_iff_of_refl theorem

[IsRefl α r] : s.Pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b

Full source

theorem pairwise_iff_of_refl [IsRefl α r] : s.Pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b :=
  forall₄_congr fun _ _ _ _ => or_iff_not_imp_left.symm.trans <| or_iff_right_of_imp of_eq

Characterization of Pairwise Relations for Reflexive Relations

Informal description

For a reflexive relation $r$ on a type $\alpha$ and a set $s \subseteq \alpha$, the following are equivalent: 1. The set $s$ is pairwise related by $r$. 2. For any elements $a, b \in s$, the relation $r(a, b)$ holds.

Set.Nonempty.pairwise_iff_exists_forall theorem

[IsEquiv α r] {s : Set ι} (hs : s.Nonempty) : s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Full source

theorem Nonempty.pairwise_iff_exists_forall [IsEquiv α r] {s : Set ι} (hs : s.Nonempty) :
    s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z := by
  constructor
  · rcases hs with ⟨y, hy⟩
    refine fun H => ⟨f y, fun x hx => ?_⟩
    rcases eq_or_ne x y with (rfl | hne)
    · apply IsRefl.refl
    · exact H hx hy hne
  · rintro ⟨z, hz⟩ x hx y hy _
    exact @IsTrans.trans α r _ (f x) z (f y) (hz _ hx) (IsSymm.symm _ _ <| hz _ hy)

Equivalence of Pairwise Relation and Universal Relation for Nonempty Sets under Equivalence Relations

Informal description

Let $r$ be an equivalence relation on a type $\alpha$, and let $s$ be a nonempty set of indices. For a function $f \colon \iota \to \alpha$, the following are equivalent: 1. The set $s$ is pairwise related by the relation $(r \text{ on } f)$, meaning that for any distinct $x, y \in s$, $r(f(x), f(y))$ holds. 2. There exists an element $z \in \alpha$ such that for every $x \in s$, $r(f(x), z)$ holds.

Set.Nonempty.pairwise_eq_iff_exists_eq theorem

{s : Set α} (hs : s.Nonempty) {f : α → ι} : (s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z

Full source

/-- 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 Nonempty.pairwise_eq_iff_exists_eq {s : Set α} (hs : s.Nonempty) {f : α → ι} :
    (s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z :=
  hs.pairwise_iff_exists_forall

Equivalence of Pairwise Equality and Constant Function on Nonempty Sets

Informal description

For a nonempty set $s$ and a function $f \colon \alpha \to \iota$, the following are equivalent: 1. The function $f$ takes pairwise equal values on $s$, meaning that for any distinct $x, y \in s$, $f(x) = f(y)$. 2. There exists an element $z \in \iota$ such that for every $x \in s$, $f(x) = z$.

Set.pairwise_iff_exists_forall theorem

 [Nonempty ι] (s : Set α) (f : α → ι) {r : ι → ι → Prop} [IsEquiv ι r] : s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z

Full source

theorem pairwise_iff_exists_forall [Nonempty ι] (s : Set α) (f : α → ι) {r : ι → ι → Prop}
    [IsEquiv ι r] : s.Pairwise (r on f) ↔ ∃ z, ∀ x ∈ s, r (f x) z := by
  rcases s.eq_empty_or_nonempty with (rfl | hne)
  · simp
  · exact hne.pairwise_iff_exists_forall

Equivalence of Pairwise Relation and Universal Relation for Nonempty Types

Informal description

Let $\iota$ be a nonempty type, $s$ a set of elements of type $\alpha$, and $f \colon \alpha \to \iota$ a function. Suppose $r$ is an equivalence relation on $\iota$. Then the following are equivalent: 1. The set $s$ is pairwise related by the relation $(r \text{ on } f)$, meaning that for any distinct $x, y \in s$, $r(f(x), f(y))$ holds. 2. There exists an element $z \in \iota$ such that for every $x \in s$, $r(f(x), z)$ holds.

Set.pairwise_eq_iff_exists_eq theorem

[Nonempty ι] (s : Set α) (f : α → ι) : (s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z

Full source

/-- 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 pairwise_eq_iff_exists_eq [Nonempty ι] (s : Set α) (f : α → ι) :
    (s.Pairwise fun x y => f x = f y) ↔ ∃ z, ∀ x ∈ s, f x = z :=
  pairwise_iff_exists_forall s f

Equivalence of Pairwise Equality and Constant Function for Nonempty Codomain

Informal description

Let $\iota$ be a nonempty type, $s$ a set of elements of type $\alpha$, and $f \colon \alpha \to \iota$ a function. Then the following are equivalent: 1. The function $f$ takes pairwise equal values on $s$, meaning that for any distinct $x, y \in s$, $f(x) = f(y)$. 2. There exists an element $z \in \iota$ such that for every $x \in s$, $f(x) = z$.

Set.pairwise_union theorem

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

Full source

theorem pairwise_union :
    (s ∪ t).Pairwise r ↔
    s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a := by
  simp only [Set.Pairwise, mem_union, or_imp, forall_and]
  aesop

Pairwise Relation on Union of Sets

Informal description

For any sets $s$ and $t$ and any symmetric relation $r$, the union $s \cup t$ satisfies the pairwise relation $r$ if and only if: 1. $s$ satisfies $r$ pairwise, 2. $t$ satisfies $r$ pairwise, and 3. For any $a \in s$ and $b \in t$ with $a \neq b$, both $r(a, b)$ and $r(b, a)$ hold.

Set.pairwise_union_of_symmetric theorem

 (hr : Symmetric r) : (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b

Full source

theorem pairwise_union_of_symmetric (hr : Symmetric r) :
    (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b :=
  pairwise_union.trans <| by simp only [hr.iff, and_self_iff]

Pairwise Relation Characterization for Union of Sets with Symmetric Relation

Informal description

For any symmetric relation $r$ and sets $s$ and $t$, the union $s \cup t$ satisfies the pairwise relation $r$ if and only if: 1. $s$ satisfies $r$ pairwise, 2. $t$ satisfies $r$ pairwise, and 3. For any $a \in s$ and $b \in t$ with $a \neq b$, the relation $r(a, b)$ holds.

Set.pairwise_insert theorem

: (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a

Full source

theorem pairwise_insert :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b ∧ r b a := by
  simp only [insert_eq, pairwise_union, pairwise_singleton, true_and, mem_singleton_iff, forall_eq]

Pairwise Relation Characterization for Insertion into a Set

Informal description

For a set $s$ and an element $a$, the pairwise relation $r$ holds on the set $\{a\} \cup s$ if and only if: 1. The relation $r$ holds pairwise on $s$, and 2. For every element $b \in s$ distinct from $a$, both $r(a, b)$ and $r(b, a)$ hold.

Set.pairwise_insert_of_not_mem theorem

(ha : a ∉ s) : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a

Full source

theorem pairwise_insert_of_not_mem (ha : a ∉ s) :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b ∧ r b a :=
  pairwise_insert.trans <|
    and_congr_right' <| forall₂_congr fun b hb => by simp [(ne_of_mem_of_not_mem hb ha).symm]

Pairwise Relation Characterization for Insertion of New Element

Informal description

For a set $s$, an element $a \notin s$, and a relation $r$, the relation $r$ holds pairwise on the set $\{a\} \cup s$ if and only if: 1. $r$ holds pairwise on $s$, and 2. For every element $b \in s$, both $r(a, b)$ and $r(b, a)$ hold.

Set.Pairwise.insert theorem

(hs : s.Pairwise r) (h : ∀ b ∈ s, a ≠ b → r a b ∧ r b a) : (insert a s).Pairwise r

Full source

protected theorem Pairwise.insert (hs : s.Pairwise r) (h : ∀ b ∈ s, a ≠ b → r a b ∧ r b a) :
    (insert a s).Pairwise r :=
  pairwise_insert.2 ⟨hs, h⟩

Pairwise Relation Preservation under Insertion

Informal description

Let $r$ be a relation on a type, $s$ a set, and $a$ an element. If: 1. The relation $r$ holds pairwise on $s$, and 2. For every $b \in s$ with $a \neq b$, both $r(a, b)$ and $r(b, a)$ hold, then the relation $r$ holds pairwise on the set $\{a\} \cup s$.

Set.Pairwise.insert_of_not_mem theorem

(ha : a ∉ s) (hs : s.Pairwise r) (h : ∀ b ∈ s, r a b ∧ r b a) : (insert a s).Pairwise r

Full source

theorem Pairwise.insert_of_not_mem (ha : a ∉ s) (hs : s.Pairwise r) (h : ∀ b ∈ s, r a b ∧ r b a) :
    (insert a s).Pairwise r :=
  (pairwise_insert_of_not_mem ha).2 ⟨hs, h⟩

Pairwise Relation Extension by Insertion of New Element

Informal description

Let $s$ be a set and $r$ a relation. If $a \notin s$, $r$ holds pairwise on $s$, and for every $b \in s$ both $r(a, b)$ and $r(b, a)$ hold, then $r$ holds pairwise on the set $\{a\} \cup s$.

Set.pairwise_insert_of_symmetric theorem

(hr : Symmetric r) : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b

Full source

theorem pairwise_insert_of_symmetric (hr : Symmetric r) :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b := by
  simp only [pairwise_insert, hr.iff a, and_self_iff]

Characterization of Pairwise Relation in Inserted Set via Symmetric Relation

Informal description

Let $r$ be a symmetric relation on a type. For any element $a$ and set $s$, the set $\{a\} \cup s$ is pairwise related under $r$ if and only if $s$ is pairwise related under $r$ and for every $b \in s$ with $a \neq b$, both $r(a, b)$ and $r(b, a)$ hold.

Set.pairwise_insert_of_symmetric_of_not_mem theorem

(hr : Symmetric r) (ha : a ∉ s) : (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b

Full source

theorem pairwise_insert_of_symmetric_of_not_mem (hr : Symmetric r) (ha : a ∉ s) :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, r a b := by
  simp only [pairwise_insert_of_not_mem ha, hr.iff a, and_self_iff]

Characterization of Pairwise Relation in Inserted Set via Symmetric Relation and Non-Membership

Informal description

Let $r$ be a symmetric relation on a type $\alpha$, and let $s$ be a set in $\alpha$ with $a \notin s$. Then the relation $r$ holds pairwise on the set $\{a\} \cup s$ if and only if: 1. $r$ holds pairwise on $s$, and 2. For every element $b \in s$, the relation $r(a, b)$ holds.

Set.Pairwise.insert_of_symmetric theorem

(hs : s.Pairwise r) (hr : Symmetric r) (h : ∀ b ∈ s, a ≠ b → r a b) : (insert a s).Pairwise r

Full source

theorem Pairwise.insert_of_symmetric (hs : s.Pairwise r) (hr : Symmetric r)
    (h : ∀ b ∈ s, a ≠ b → r a b) : (insert a s).Pairwise r :=
  (pairwise_insert_of_symmetric hr).2 ⟨hs, h⟩

Pairwise Relation Preservation under Insertion with Symmetric Relation

Informal description

Let $r$ be a symmetric relation on a type $\alpha$, and let $s$ be a set in $\alpha$ that is pairwise related under $r$. If for every element $b \in s$ with $a \neq b$, the relation $r(a, b)$ holds, then the set $\{a\} \cup s$ is also pairwise related under $r$.

Set.Pairwise.insert_of_symmetric_of_not_mem theorem

(hs : s.Pairwise r) (hr : Symmetric r) (ha : a ∉ s) (h : ∀ b ∈ s, r a b) : (insert a s).Pairwise r

Full source

@[deprecated Pairwise.insert_of_symmetric (since := "2025-03-19")]
theorem Pairwise.insert_of_symmetric_of_not_mem (hs : s.Pairwise r) (hr : Symmetric r) (ha : a ∉ s)
    (h : ∀ b ∈ s, r a b) : (insert a s).Pairwise r :=
  (pairwise_insert_of_symmetric_of_not_mem hr ha).2 ⟨hs, h⟩

Pairwise Relation Extension via Insertion with Symmetric Relation and Non-Membership

Informal description

Let $r$ be a symmetric relation on a type $\alpha$, and let $s$ be a set in $\alpha$ that is pairwise related under $r$. If $a \notin s$ and for every element $b \in s$ the relation $r(a, b)$ holds, then the set $\{a\} \cup s$ is also pairwise related under $r$.

Set.pairwise_pair theorem

: Set.Pairwise { a, b } r ↔ a ≠ b → r a b ∧ r b a

Full source

theorem pairwise_pair : Set.PairwiseSet.Pairwise {a, b} r ↔ a ≠ b → r a b ∧ r b a := by simp [pairwise_insert]

Pairwise Relation on Two-Element Set

Informal description

For any binary relation $r$ on a type $\alpha$, the set $\{a, b\}$ is pairwise related under $r$ if and only if whenever $a \neq b$, both $r(a, b)$ and $r(b, a)$ hold.

Set.pairwise_pair_of_symmetric theorem

(hr : Symmetric r) : Set.Pairwise { a, b } r ↔ a ≠ b → r a b

Full source

theorem pairwise_pair_of_symmetric (hr : Symmetric r) : Set.PairwiseSet.Pairwise {a, b} r ↔ a ≠ b → r a b := by
  simp [pairwise_insert_of_symmetric hr]

Pairwise relation on a pair via symmetric relation

Informal description

For a symmetric relation $r$ on a type $\alpha$, the set $\{a, b\}$ is pairwise related under $r$ if and only if whenever $a \neq b$, the relation $r(a, b)$ holds.

Set.pairwise_univ theorem

: (univ : Set α).Pairwise r ↔ Pairwise r

Full source

theorem pairwise_univ : (univ : Set α).Pairwise r ↔ Pairwise r := by
  simp only [Set.Pairwise, Pairwise, mem_univ, forall_const]

Universal Set Pairwise Property Equivalence

Informal description

For any relation $r$ on a type $\alpha$, the universal set `univ` (containing all elements of $\alpha$) satisfies the pairwise property with respect to $r$ if and only if the relation $r$ holds pairwise on all elements of $\alpha$.

Set.pairwise_bot_iff theorem

: s.Pairwise (⊥ : α → α → Prop) ↔ (s : Set α).Subsingleton

Full source

@[simp]
theorem pairwise_bot_iff : s.Pairwise (⊥ : α → α → Prop) ↔ (s : Set α).Subsingleton :=
  ⟨fun h _a ha _b hb => h.eq ha hb id, fun h => h.pairwise _⟩

Pairwise False Relation Characterizes Subsingleton Sets

Informal description

For any set $s$ of elements of type $\alpha$, the relation $\bot$ (the always-false relation) holds pairwise on $s$ if and only if $s$ is a subsingleton (i.e., has at most one element). In other words, $s$ is pairwise $\bot$ if and only if $s$ contains at most one element.

Set.injOn_iff_pairwise_ne theorem

{s : Set ι} : InjOn f s ↔ s.Pairwise (f · ≠ f ·)

Full source

/-- See also `Function.injective_iff_pairwise_ne` -/
lemma injOn_iff_pairwise_ne {s : Set ι} : InjOnInjOn f s ↔ s.Pairwise (f · ≠ f ·) := by
  simp only [InjOn, Set.Pairwise, not_imp_not]

Injectivity on a Set is Equivalent to Pairwise Distinct Images

Informal description

For a function $f$ defined on a set $s$ with elements of type $\iota$, the function $f$ is injective on $s$ if and only if for any two distinct elements $x, y \in s$, the images $f(x)$ and $f(y)$ are distinct. In other words, $\text{InjOn}(f, s) \leftrightarrow \text{Pairwise}(s, \lambda x y, f(x) \neq f(y))$.

Set.Pairwise.image theorem

{s : Set ι} (h : s.Pairwise (r on f)) : (f '' s).Pairwise r

Full source

protected theorem Pairwise.image {s : Set ι} (h : s.Pairwise (r on f)) : (f '' s).Pairwise r :=
  forall_mem_image.2 fun _x hx ↦ forall_mem_image.2 fun _y hy hne ↦ h hx hy <| ne_of_apply_ne _ hne

Pairwise Relation Preservation under Function Image

Informal description

Let $s$ be a set of elements of type $\iota$, and let $r$ be a binary relation on the codomain of a function $f \colon \iota \to \alpha$. If $s$ satisfies the pairwise relation $(r \text{ on } f)$, meaning that for any two distinct elements $x, y \in s$, the relation $r(f(x), f(y))$ holds, then the image $f(s)$ satisfies the pairwise relation $r$.

Set.InjOn.pairwise_image theorem

{s : Set ι} (h : s.InjOn f) : (f '' s).Pairwise r ↔ s.Pairwise (r on f)

Full source

/-- See also `Set.Pairwise.image`. -/
theorem InjOn.pairwise_image {s : Set ι} (h : s.InjOn f) :
    (f '' s).Pairwise r ↔ s.Pairwise (r on f) := by
  simp +contextual [h.eq_iff, Set.Pairwise]

Equivalence of Pairwise Relations on Image and Preimage under Injective Function

Informal description

Let $s$ be a set of elements of type $\iota$ and $f \colon \iota \to \alpha$ be a function. If $f$ is injective on $s$, then the following are equivalent: 1. The relation $r$ holds pairwise for all distinct elements in the image $f(s)$. 2. The relation $r$ holds pairwise for all distinct elements $x, y \in s$ when applied to their images, i.e., $r(f(x), f(y))$ holds.

Pairwise.range_pairwise theorem

(hr : Pairwise (r on f)) : (Set.range f).Pairwise r

Full source

lemma _root_.Pairwise.range_pairwise (hr : Pairwise (r on f)) : (Set.range f).Pairwise r :=
  image_univ ▸ (pairwise_univ.mpr hr).image

Pairwise Relation on Function Range from Pairwise Relation on Function Inputs

Informal description

Let $f \colon \alpha \to \beta$ be a function and $r$ a binary relation on $\beta$. If the relation $r$ holds pairwise for all pairs $(f(x), f(y))$ with $x \neq y$ in $\alpha$, then the relation $r$ holds pairwise for all distinct elements in the range of $f$.

pairwise_subtype_iff_pairwise_set theorem

(s : Set α) (r : α → α → Prop) : (Pairwise fun (x : s) (y : s) => r x y) ↔ s.Pairwise r

Full source

theorem pairwise_subtype_iff_pairwise_set (s : Set α) (r : α → α → Prop) :
    (Pairwise fun (x : s) (y : s) => r x y) ↔ s.Pairwise r := by
  simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne, Subtype.ext_iff, Subtype.coe_mk]

Equivalence of Pairwise Relations on Subtypes and Sets

Informal description

For any set $s$ of elements of type $\alpha$ and any binary relation $r$ on $\alpha$, the following are equivalent: 1. The relation $r$ holds pairwise for all pairs of elements in the subtype corresponding to $s$. 2. The relation $r$ holds pairwise for all pairs of distinct elements in $s$.

Set.PairwiseDisjoint definition

(s : Set ι) (f : ι → α) : Prop

Full source

/-- 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. -/
def PairwiseDisjoint (s : Set ι) (f : ι → α) : Prop :=
  s.Pairwise (DisjointDisjoint on f)

Pairwise disjoint sets under a function

Informal description

A set $s$ of elements of type $\iota$ is called *pairwise disjoint* with respect to a function $f \colon \iota \to \alpha$ if for any two distinct elements $i, j \in s$, the images $f(i)$ and $f(j)$ are disjoint. More formally, $s$ is pairwise disjoint under $f$ if for all $i, j \in s$ with $i \neq j$, we have $f(i) \cap f(j) = \emptyset$ (or the appropriate notion of disjointness in $\alpha$).

Set.PairwiseDisjoint.subset theorem

(ht : t.PairwiseDisjoint f) (h : s ⊆ t) : s.PairwiseDisjoint f

Full source

theorem PairwiseDisjoint.subset (ht : t.PairwiseDisjoint f) (h : s ⊆ t) : s.PairwiseDisjoint f :=
  Pairwise.mono h ht

Subset Preserves Pairwise Disjointness

Informal description

Let $s$ and $t$ be sets of indices of type $\iota$, and let $f \colon \iota \to \alpha$ be a function. If $t$ is pairwise disjoint under $f$ and $s$ is a subset of $t$, then $s$ is also pairwise disjoint under $f$.

Set.PairwiseDisjoint.mono_on theorem

(hs : s.PairwiseDisjoint f) (h : ∀ ⦃i⦄, i ∈ s → g i ≤ f i) : s.PairwiseDisjoint g

Full source

theorem PairwiseDisjoint.mono_on (hs : s.PairwiseDisjoint f) (h : ∀ ⦃i⦄, i ∈ s → g i ≤ f i) :
    s.PairwiseDisjoint g := fun _a ha _b hb hab => (hs ha hb hab).mono (h ha) (h hb)

Monotonicity of Pairwise Disjointness under Pointwise Inequality

Informal description

Let $s$ be a set of indices and $f, g$ be functions from the index set to a type $\alpha$ with a partial order and a bottom element. If $s$ is pairwise disjoint under $f$ and for every $i \in s$ we have $g(i) \leq f(i)$, then $s$ is also pairwise disjoint under $g$.

Set.PairwiseDisjoint.mono theorem

(hs : s.PairwiseDisjoint f) (h : g ≤ f) : s.PairwiseDisjoint g

Full source

theorem PairwiseDisjoint.mono (hs : s.PairwiseDisjoint f) (h : g ≤ f) : s.PairwiseDisjoint g :=
  hs.mono_on fun i _ => h i

Monotonicity of Pairwise Disjointness under Pointwise Inequality (Global Version)

Informal description

Let $s$ be a set of indices and $f, g \colon \iota \to \alpha$ be functions to a type $\alpha$ with a partial order and a bottom element. If $s$ is pairwise disjoint under $f$ and $g(i) \leq f(i)$ for all $i \in \iota$, then $s$ is also pairwise disjoint under $g$.

Set.pairwiseDisjoint_empty theorem

: (∅ : Set ι).PairwiseDisjoint f

Full source

@[simp]
theorem pairwiseDisjoint_empty : (∅ : Set ι).PairwiseDisjoint f :=
  pairwise_empty _

Empty Set is Pairwise Disjoint Under Any Function

Informal description

For any function $f \colon \iota \to \alpha$, the empty set $\emptyset \subseteq \iota$ is pairwise disjoint under $f$.

Set.pairwiseDisjoint_singleton theorem

(i : ι) (f : ι → α) : PairwiseDisjoint { i } f

Full source

@[simp]
theorem pairwiseDisjoint_singleton (i : ι) (f : ι → α) : PairwiseDisjoint {i} f :=
  pairwise_singleton i _

Singleton Sets are Pairwise Disjoint Under Any Function

Informal description

For any element $i$ of type $\iota$ and any function $f \colon \iota \to \alpha$, the singleton set $\{i\}$ is pairwise disjoint under $f$.

Set.pairwiseDisjoint_insert theorem

{i : ι} : (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)

Full source

theorem pairwiseDisjoint_insert {i : ι} :
    (insert i s).PairwiseDisjoint f ↔
      s.PairwiseDisjoint f ∧ ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j) :=
  pairwise_insert_of_symmetric <| symmetric_disjoint.comap f

Characterization of Pairwise Disjointness in Inserted Set

Informal description

For any element $i$ of type $\iota$ and any function $f \colon \iota \to \alpha$, the set $\{i\} \cup s$ is pairwise disjoint under $f$ if and only if $s$ is pairwise disjoint under $f$ and for every $j \in s$ with $i \neq j$, the images $f(i)$ and $f(j)$ are disjoint.

Set.pairwiseDisjoint_insert_of_not_mem theorem

 {i : ι} (hi : i ∉ s) : (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j)

Full source

theorem pairwiseDisjoint_insert_of_not_mem {i : ι} (hi : i ∉ s) :
    (insert i s).PairwiseDisjoint f ↔ s.PairwiseDisjoint f ∧ ∀ j ∈ s, Disjoint (f i) (f j) :=
  pairwise_insert_of_symmetric_of_not_mem (symmetric_disjoint.comap f) hi

Characterization of pairwise disjointness when inserting a new element into a set

Informal description

For any element $i$ of type $\iota$ not in the set $s$, and any function $f \colon \iota \to \alpha$, the set $\{i\} \cup s$ is pairwise disjoint under $f$ if and only if: 1. $s$ is pairwise disjoint under $f$, and 2. For every $j \in s$, the images $f(i)$ and $f(j)$ are disjoint.

Set.PairwiseDisjoint.insert theorem

 (hs : s.PairwiseDisjoint f) {i : ι} (h : ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)) : (insert i s).PairwiseDisjoint f

Full source

protected theorem PairwiseDisjoint.insert (hs : s.PairwiseDisjoint f) {i : ι}
    (h : ∀ j ∈ s, i ≠ j → Disjoint (f i) (f j)) : (insert i s).PairwiseDisjoint f :=
  pairwiseDisjoint_insert.2 ⟨hs, h⟩

Insertion Preserves Pairwise Disjointness

Informal description

Let $s$ be a set of indices of type $\iota$, and let $f \colon \iota \to \alpha$ be a function. If $s$ is pairwise disjoint under $f$, and for a new index $i \notin s$, the images $f(i)$ and $f(j)$ are disjoint for all $j \in s$ with $i \neq j$, then the set $\{i\} \cup s$ is also pairwise disjoint under $f$.

Set.PairwiseDisjoint.insert_of_not_mem theorem

 (hs : s.PairwiseDisjoint f) {i : ι} (hi : i ∉ s) (h : ∀ j ∈ s, Disjoint (f i) (f j)) : (insert i s).PairwiseDisjoint f

Full source

theorem PairwiseDisjoint.insert_of_not_mem (hs : s.PairwiseDisjoint f) {i : ι} (hi : i ∉ s)
    (h : ∀ j ∈ s, Disjoint (f i) (f j)) : (insert i s).PairwiseDisjoint f :=
  (pairwiseDisjoint_insert_of_not_mem hi).2 ⟨hs, h⟩

Insertion Preserves Pairwise Disjointness for Non-Member Elements

Informal description

Let $s$ be a set of indices of type $\iota$, and let $f \colon \iota \to \alpha$ be a function. If $s$ is pairwise disjoint under $f$, and for a new index $i \notin s$, the images $f(i)$ and $f(j)$ are disjoint for all $j \in s$, then the set $\{i\} \cup s$ is also pairwise disjoint under $f$.

Set.PairwiseDisjoint.image_of_le theorem

(hs : s.PairwiseDisjoint f) {g : ι → ι} (hg : f ∘ g ≤ f) : (g '' s).PairwiseDisjoint f

Full source

theorem PairwiseDisjoint.image_of_le (hs : s.PairwiseDisjoint f) {g : ι → ι} (hg : f ∘ g ≤ f) :
    (g '' s).PairwiseDisjoint f := by
  rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ h
  exact (hs ha hb <| ne_of_apply_ne _ h).mono (hg a) (hg b)

Image of Pairwise Disjoint Set under Monotone Function Preserves Pairwise Disjointness

Informal description

Let $s$ be a set of indices of type $\iota$, and let $f \colon \iota \to \alpha$ be a function. If $s$ is pairwise disjoint under $f$, and $g \colon \iota \to \iota$ is a function such that $f \circ g \leq f$ (i.e., $f(g(i)) \leq f(i)$ for all $i \in \iota$), then the image of $s$ under $g$ is also pairwise disjoint under $f$.

Set.InjOn.pairwiseDisjoint_image theorem

{g : ι' → ι} {s : Set ι'} (h : s.InjOn g) : (g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g)

Full source

theorem InjOn.pairwiseDisjoint_image {g : ι' → ι} {s : Set ι'} (h : s.InjOn g) :
    (g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g) :=
  h.pairwise_image

Equivalence of Pairwise Disjointness for Image and Preimage under Injective Function

Informal description

Let $g \colon \iota' \to \iota$ be a function and $s$ be a set in $\iota'$. If $g$ is injective on $s$, then the image set $g(s)$ is pairwise disjoint with respect to a function $f \colon \iota \to \alpha$ if and only if $s$ is pairwise disjoint with respect to the composition $f \circ g$.

Set.PairwiseDisjoint.range theorem

(g : s → ι) (hg : ∀ i : s, f (g i) ≤ f i) (ht : s.PairwiseDisjoint f) : (range g).PairwiseDisjoint f

Full source

theorem PairwiseDisjoint.range (g : s → ι) (hg : ∀ i : s, f (g i) ≤ f i)
    (ht : s.PairwiseDisjoint f) : (range g).PairwiseDisjoint f := by
  rintro _ ⟨x, rfl⟩ _ ⟨y, rfl⟩ hxy
  exact ((ht x.2 y.2) fun h => hxy <| congr_arg g <| Subtype.ext h).mono (hg x) (hg y)

Range of a Function Preserves Pairwise Disjointness Under Monotonicity Condition

Informal description

Let $s$ be a set of indices of type $\iota$, and let $f \colon \iota \to \alpha$ be a function. Suppose $g \colon s \to \iota$ is a function such that for every $i \in s$, $f(g(i)) \leq f(i)$. If $s$ is pairwise disjoint under $f$, then the range of $g$ is also pairwise disjoint under $f$.

Set.pairwiseDisjoint_union theorem

 :
  (s ∪ t).PairwiseDisjoint f ↔
    s.PairwiseDisjoint f ∧ t.PairwiseDisjoint f ∧ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j)

Full source

theorem pairwiseDisjoint_union :
    (s ∪ t).PairwiseDisjoint f ↔
      s.PairwiseDisjoint f ∧
        t.PairwiseDisjoint f ∧ ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ t → i ≠ j → Disjoint (f i) (f j) :=
  pairwise_union_of_symmetric <| symmetric_disjoint.comap f

Characterization of Pairwise Disjointness for Union of Sets

Informal description

For any sets $s$ and $t$ and any function $f \colon \iota \to \alpha$, the union $s \cup t$ is pairwise disjoint under $f$ if and only if: 1. $s$ is pairwise disjoint under $f$, 2. $t$ is pairwise disjoint under $f$, and 3. For any $i \in s$ and $j \in t$ with $i \neq j$, the images $f(i)$ and $f(j)$ are disjoint.

Set.PairwiseDisjoint.union theorem

 (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

Full source

theorem PairwiseDisjoint.union (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 :=
  pairwiseDisjoint_union.2 ⟨hs, ht, h⟩

Union of Pairwise Disjoint Sets is Pairwise Disjoint

Informal description

Let $s$ and $t$ be sets of indices, and let $f \colon \iota \to \alpha$ be a function. If: 1. $s$ is pairwise disjoint under $f$, 2. $t$ is pairwise disjoint under $f$, and 3. For any $i \in s$ and $j \in t$ with $i \neq j$, the images $f(i)$ and $f(j)$ are disjoint, then the union $s \cup t$ is pairwise disjoint under $f$.

Set.PairwiseDisjoint.elim theorem

(hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (h : ¬Disjoint (f i) (f j)) : i = j

Full source

theorem PairwiseDisjoint.elim (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
    (h : ¬Disjoint (f i) (f j)) : i = j :=
  hs.eq hi hj h

Equality of Indices for Non-Disjoint Images in Pairwise Disjoint Sets

Informal description

Let $s$ be a set of indices, and let $f \colon \iota \to \alpha$ be a function. If $s$ is pairwise disjoint under $f$, then for any two indices $i, j \in s$ such that $f(i)$ and $f(j)$ are not disjoint, we have $i = j$.

Set.pairwiseDisjoint_range_iff theorem

{α β : Type*} {f : α → (Set β)} : (range f).PairwiseDisjoint id ↔ ∀ x y, f x ≠ f y → Disjoint (f x) (f y)

Full source

lemma pairwiseDisjoint_range_iff {α β : Type*} {f : α → (Set β)} :
    (range f).PairwiseDisjoint id ↔ ∀ x y, f x ≠ f y → Disjoint (f x) (f y) := by
  aesop (add simp [PairwiseDisjoint, Set.Pairwise])

Characterization of Pairwise Disjointness in the Range of a Set-Valued Function

Informal description

For any function $f \colon \alpha \to \text{Set } \beta$, the range of $f$ is pairwise disjoint under the identity function if and only if for any two elements $x, y \in \alpha$, if $f(x) \neq f(y)$, then $f(x)$ and $f(y)$ are disjoint sets.

Pairwise.pairwiseDisjoint theorem

(h : Pairwise (Disjoint on f)) (s : Set ι) : s.PairwiseDisjoint f

Full source

/-- If the range of `f` is pairwise disjoint, then the image of any set `s` under `f` is as well. -/
lemma _root_.Pairwise.pairwiseDisjoint (h : Pairwise (DisjointDisjoint on f)) (s : Set ι) :
    s.PairwiseDisjoint f := h.set_pairwise s

Pairwise Disjointness is Preserved under Subsets

Informal description

If the images of any two distinct elements under a function $f \colon \iota \to \alpha$ are disjoint (i.e., the family $\{f(i)\}_{i \in \iota}$ is pairwise disjoint), then for any subset $s \subseteq \iota$, the images $\{f(i)\}_{i \in s}$ are also pairwise disjoint.

Set.PairwiseDisjoint.elim' theorem

(hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s) (h : f i ⊓ f j ≠ ⊥) : i = j

Full source

theorem PairwiseDisjoint.elim' (hs : s.PairwiseDisjoint f) {i j : ι} (hi : i ∈ s) (hj : j ∈ s)
    (h : f i ⊓ f jf i ⊓ f j ≠ ⊥) : i = j :=
  (hs.elim hi hj) fun hij => h hij.eq_bot

Equality of Indices for Non-Bottom Infimum in Pairwise Disjoint Sets

Informal description

Let $s$ be a set of indices and $f \colon \iota \to \alpha$ a function such that $s$ is pairwise disjoint under $f$. For any two indices $i, j \in s$ with $f(i) \sqcap f(j) \neq \bot$, we have $i = j$.

Set.pairwiseDisjoint_range_singleton theorem

: (range (singleton : ι → Set ι)).PairwiseDisjoint id

Full source

theorem pairwiseDisjoint_range_singleton :
    (range (singleton : ι → Set ι)).PairwiseDisjoint id :=
  Pairwise.range_pairwise fun _ _ => disjoint_singleton.2

Pairwise Disjointness of Singleton Sets' Range

Informal description

The range of the singleton function $\iota \to \text{Set } \iota$, which maps each element $i \in \iota$ to the singleton set $\{i\}$, is pairwise disjoint with respect to the identity function. That is, for any two distinct singleton sets $\{i\}$ and $\{j\}$ in the range, their intersection is empty.

Set.pairwiseDisjoint_fiber theorem

(f : ι → α) (s : Set α) : s.PairwiseDisjoint fun a => f ⁻¹' { a }

Full source

theorem pairwiseDisjoint_fiber (f : ι → α) (s : Set α) : s.PairwiseDisjoint fun a => f ⁻¹' {a} :=
  fun _a _ _b _ h => disjoint_iff_inf_le.mpr fun _i ⟨hia, hib⟩ => h <| (Eq.symm hia).trans hib

Preimages of distinct singletons under a function are pairwise disjoint

Informal description

For any function $f \colon \iota \to \alpha$ and any subset $s \subseteq \alpha$, the preimages $f^{-1}(\{a\})$ for $a \in s$ are pairwise disjoint. That is, for any distinct $a, b \in s$, the sets $f^{-1}(\{a\})$ and $f^{-1}(\{b\})$ are disjoint.

Set.PairwiseDisjoint.elim_set theorem

 {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

Full source

theorem PairwiseDisjoint.elim_set {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 :=
  hs.elim hi hj <| not_disjoint_iff.2 ⟨a, hai, haj⟩

Equality of Indices for Common Elements in Pairwise Disjoint Sets

Informal description

Let $s$ be a set of indices, and let $f \colon \iota \to \mathcal{P}(\alpha)$ be a function mapping each index to a subset of $\alpha$. If $s$ is pairwise disjoint under $f$, then for any two indices $i, j \in s$ and any element $a \in \alpha$ such that $a \in f(i)$ and $a \in f(j)$, we have $i = j$.

Set.PairwiseDisjoint.prod theorem

 {f : ι → Set α} {g : ι' → Set β} (hs : s.PairwiseDisjoint f) (ht : t.PairwiseDisjoint g) :
  (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2

Full source

theorem PairwiseDisjoint.prod {f : ι → Set α} {g : ι' → Set β} (hs : s.PairwiseDisjoint f)
    (ht : t.PairwiseDisjoint g) :
    (s ×ˢ t : Set (ι × ι')).PairwiseDisjoint fun i => f i.1 ×ˢ g i.2 :=
  fun ⟨_, _⟩ ⟨hi, hi'⟩ ⟨_, _⟩ ⟨hj, hj'⟩ hij =>
  disjoint_left.2 fun ⟨_, _⟩ ⟨hai, hbi⟩ ⟨haj, hbj⟩ =>
    hij <| Prod.ext (hs.elim_set hi hj _ hai haj) <| ht.elim_set hi' hj' _ hbi hbj

Pairwise Disjointness Preserved Under Cartesian Product of Sets

Informal description

Let $f \colon \iota \to \mathcal{P}(\alpha)$ and $g \colon \iota' \to \mathcal{P}(\beta)$ be functions mapping indices to sets, and let $s \subseteq \iota$ and $t \subseteq \iota'$ be sets of indices. If $s$ is pairwise disjoint under $f$ and $t$ is pairwise disjoint under $g$, then the Cartesian product $s \times t$ is pairwise disjoint under the function $(i, j) \mapsto f(i) \times g(j)$.

Set.pairwiseDisjoint_pi theorem

 {ι' α : ι → Type*} {s : ∀ i, Set (ι' i)} {f : ∀ i, ι' i → Set (α i)} (hs : ∀ i, (s i).PairwiseDisjoint (f i)) :
  ((univ : Set ι).pi s).PairwiseDisjoint fun I => (univ : Set ι).pi fun i => f _ (I i)

Full source

theorem pairwiseDisjoint_pi {ι' α : ι → Type*} {s : ∀ i, Set (ι' i)} {f : ∀ i, ι' i → Set (α i)}
    (hs : ∀ i, (s i).PairwiseDisjoint (f i)) :
    ((univ : Set ι).pi s).PairwiseDisjoint fun I => (univ : Set ι).pi fun i => f _ (I i) :=
  fun _ hI _ hJ hIJ =>
  disjoint_left.2 fun a haI haJ =>
    hIJ <|
      funext fun i =>
        (hs i).elim_set (hI i trivial) (hJ i trivial) (a i) (haI i trivial) (haJ i trivial)

Pairwise Disjointness of Product Sets under Componentwise Functions

Informal description

Let $\{ \iota'_\iota, \alpha_\iota \}_{\iota \in \iota}$ be a family of types indexed by $\iota$, and for each $i \in \iota$, let $s_i \subseteq \iota'_i$ be a set and $f_i \colon \iota'_i \to \mathcal{P}(\alpha_i)$ a function. If for every $i \in \iota$, the set $s_i$ is pairwise disjoint under $f_i$, then the product set $\prod_{i \in \iota} s_i$ is pairwise disjoint under the function $I \mapsto \prod_{i \in \iota} f_i (I(i))$.

Set.pairwiseDisjoint_image_right_iff theorem

 {f : α → β → γ} {s : Set α} {t : Set β} (hf : ∀ a ∈ s, Injective (f a)) :
  (s.PairwiseDisjoint fun a => f a '' t) ↔ (s ×ˢ t).InjOn fun p => f p.1 p.2

Full source

/-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
disjoint iff `f` is injective . -/
theorem pairwiseDisjoint_image_right_iff {f : α → β → γ} {s : Set α} {t : Set β}
    (hf : ∀ a ∈ s, Injective (f a)) :
    (s.PairwiseDisjoint fun a => f a '' t) ↔ (s ×ˢ t).InjOn fun p => f p.1 p.2 := by
  refine ⟨fun hs x hx y hy (h : f _ _ = _) => ?_, fun hs x hx y hy h => ?_⟩
  · suffices x.1 = y.1 by exact Prod.ext this (hf _ hx.1 <| h.trans <| by rw [this])
    refine hs.elim hx.1 hy.1 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.2, ?_⟩)
    rw [h]
    exact mem_image_of_mem _ hy.2
  · refine disjoint_iff_inf_le.mpr ?_
    rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
    exact h (congr_arg Prod.fst <| hs (mk_mem_prod hx ha) (mk_mem_prod hy hb) hab)

Equivalence of Pairwise Disjoint Images and Injectivity on Product Set

Informal description

Let $f \colon \alpha \to \beta \to \gamma$ be a function, $s \subseteq \alpha$ a set, and $t \subseteq \beta$ a set. Suppose that for every $a \in s$, the partial function $f(a) \colon \beta \to \gamma$ is injective. Then the following are equivalent: 1. The family of images $\{f(a) '' t\}_{a \in s}$ is pairwise disjoint. 2. The function $(a, b) \mapsto f(a)(b)$ is injective on $s \times t$.

Set.pairwiseDisjoint_image_left_iff theorem

 {f : α → β → γ} {s : Set α} {t : Set β} (hf : ∀ b ∈ t, Injective fun a => f a b) :
  (t.PairwiseDisjoint fun b => (fun a => f a b) '' s) ↔ (s ×ˢ t).InjOn fun p => f p.1 p.2

Full source

/-- The partial images of a binary function `f` whose partial evaluations are injective are pairwise
disjoint iff `f` is injective . -/
theorem pairwiseDisjoint_image_left_iff {f : α → β → γ} {s : Set α} {t : Set β}
    (hf : ∀ b ∈ t, Injective fun a => f a b) :
    (t.PairwiseDisjoint fun b => (fun a => f a b) '' s) ↔ (s ×ˢ t).InjOn fun p => f p.1 p.2 := by
  refine ⟨fun ht x hx y hy (h : f _ _ = _) => ?_, fun ht x hx y hy h => ?_⟩
  · suffices x.2 = y.2 by exact Prod.ext (hf _ hx.2 <| h.trans <| by rw [this]) this
    refine ht.elim hx.2 hy.2 (not_disjoint_iff.2 ⟨_, mem_image_of_mem _ hx.1, ?_⟩)
    rw [h]
    exact mem_image_of_mem _ hy.1
  · refine disjoint_iff_inf_le.mpr ?_
    rintro _ ⟨⟨a, ha, hab⟩, b, hb, rfl⟩
    exact h (congr_arg Prod.snd <| ht (mk_mem_prod ha hx) (mk_mem_prod hb hy) hab)

Pairwise Disjoint Images of Partial Functions vs. Injectivity on Product Set

Informal description

Let $f \colon \alpha \to \beta \to \gamma$ be a binary function, $s \subseteq \alpha$ a subset of $\alpha$, and $t \subseteq \beta$ a subset of $\beta$. Suppose that for every $b \in t$, the partial function $f(\cdot, b) \colon \alpha \to \gamma$ is injective. Then the following are equivalent: 1. The family of images $\{f(a, b) \mid a \in s\}$ for $b \in t$ is pairwise disjoint in $\gamma$. 2. The function $(a, b) \mapsto f(a, b)$ is injective on the product set $s \times t$.

Set.exists_ne_mem_inter_of_not_pairwiseDisjoint theorem

{f : ι → Set α} (h : ¬s.PairwiseDisjoint f) : ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x : α, x ∈ f i ∩ f j

Full source

lemma exists_ne_mem_inter_of_not_pairwiseDisjoint
    {f : ι → Set α} (h : ¬ s.PairwiseDisjoint f) :
    ∃ i ∈ s, ∃ j ∈ s, i ≠ j ∧ ∃ x : α, x ∈ f i ∩ f j := by
  change ¬ ∀ i, i ∈ s → ∀ j, j ∈ s → i ≠ j → ∀ t, t ≤ f i → t ≤ f j → t ≤ ⊥ at h
  simp only [not_forall] at h
  obtain ⟨i, hi, j, hj, h_ne, t, hfi, hfj, ht⟩ := h
  replace ht : t.Nonempty := by
    rwa [le_bot_iff, bot_eq_empty, ← Ne, ← nonempty_iff_ne_empty] at ht
  obtain ⟨x, hx⟩ := ht
  exact ⟨i, hi, j, hj, h_ne, x, hfi hx, hfj hx⟩

Existence of Non-Disjoint Pair in Non-Pairwise Disjoint Family

Informal description

For a set $s$ and a function $f \colon \iota \to \mathcal{P}(\alpha)$, if $s$ is not pairwise disjoint under $f$, then there exist distinct elements $i, j \in s$ and an element $x \in \alpha$ such that $x$ belongs to both $f(i)$ and $f(j)$.

Set.exists_lt_mem_inter_of_not_pairwiseDisjoint theorem

 [LinearOrder ι] {f : ι → Set α} (h : ¬s.PairwiseDisjoint f) : ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j

Full source

lemma exists_lt_mem_inter_of_not_pairwiseDisjoint [LinearOrder ι]
    {f : ι → Set α} (h : ¬ s.PairwiseDisjoint f) :
    ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j := by
  obtain ⟨i, hi, j, hj, hne, x, hx₁, hx₂⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
  rcases lt_or_lt_iff_ne.mpr hne with h_lt | h_lt
  · exact ⟨i, hi, j, hj, h_lt, x, hx₁, hx₂⟩
  · exact ⟨j, hj, i, hi, h_lt, x, hx₂, hx₁⟩

Existence of Ordered Non-Disjoint Pair in Non-Pairwise Disjoint Family

Informal description

Let $\iota$ be a linearly ordered type and $\alpha$ be any type. Given a set $s \subseteq \iota$ and a function $f \colon \iota \to \mathcal{P}(\alpha)$, if $s$ is not pairwise disjoint under $f$, then there exist elements $i, j \in s$ with $i < j$ and an element $x \in \alpha$ such that $x$ belongs to both $f(i)$ and $f(j)$.

exists_ne_mem_inter_of_not_pairwise_disjoint theorem

{f : ι → Set α} (h : ¬Pairwise (Disjoint on f)) : ∃ i j : ι, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j

Full source

lemma exists_ne_mem_inter_of_not_pairwise_disjoint
    {f : ι → Set α} (h : ¬ Pairwise (Disjoint on f)) :
    ∃ i j : ι, i ≠ j ∧ ∃ x, x ∈ f i ∩ f j := by
  rw [← pairwise_univ] at h
  obtain ⟨i, _hi, j, _hj, h⟩ := exists_ne_mem_inter_of_not_pairwiseDisjoint h
  exact ⟨i, j, h⟩

Existence of Non-Disjoint Pair in Non-Pairwise Disjoint Family of Sets

Informal description

For a family of sets $\{f(i)\}_{i \in \iota}$ indexed by $\iota$, if the family is not pairwise disjoint, then there exist distinct indices $i, j \in \iota$ and an element $x$ such that $x$ belongs to both $f(i)$ and $f(j)$.

exists_lt_mem_inter_of_not_pairwise_disjoint theorem

 [LinearOrder ι] {f : ι → Set α} (h : ¬Pairwise (Disjoint on f)) : ∃ i j : ι, i < j ∧ ∃ x, x ∈ f i ∩ f j

Full source

lemma exists_lt_mem_inter_of_not_pairwise_disjoint [LinearOrder ι]
    {f : ι → Set α} (h : ¬ Pairwise (Disjoint on f)) :
    ∃ i j : ι, i < j ∧ ∃ x, x ∈ f i ∩ f j := by
  rw [← pairwise_univ] at h
  obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h
  exact ⟨i, j, h⟩

Existence of Ordered Non-Disjoint Pair in Non-Pairwise Disjoint Family of Sets

Informal description

Let $\iota$ be a linearly ordered type and $\{f(i)\}_{i \in \iota}$ be a family of sets in $\alpha$. If the family is not pairwise disjoint, then there exist indices $i, j \in \iota$ with $i < j$ and an element $x \in \alpha$ such that $x$ belongs to both $f(i)$ and $f(j)$.

pairwise_disjoint_fiber theorem

(f : ι → α) : Pairwise (Disjoint on fun a : α => f ⁻¹' { a })

Full source

theorem pairwise_disjoint_fiber (f : ι → α) : Pairwise (DisjointDisjoint on fun a : α => f ⁻¹' {a}) :=
  pairwise_univ.1 <| Set.pairwiseDisjoint_fiber f univ

Pairwise Disjointness of Fibers under a Function

Informal description

For any function $f \colon \iota \to \alpha$, the family of preimages $\{f^{-1}(\{a\})\}_{a \in \alpha}$ is pairwise disjoint. That is, for any distinct elements $a, b \in \alpha$, the sets $f^{-1}(\{a\})$ and $f^{-1}(\{b\})$ are disjoint.

subsingleton_setOf_mem_iff_pairwise_disjoint theorem

{f : ι → Set α} : (∀ a, {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Disjoint on f)

Full source

lemma subsingleton_setOf_mem_iff_pairwise_disjoint {f : ι → Set α} :
    (∀ a, {i | a ∈ f i}.Subsingleton) ↔ Pairwise (Disjoint on f) :=
  ⟨fun h _ _ hij ↦ disjoint_left.2 fun a hi hj ↦ hij (h a hi hj),
   fun h _ _ hx _ hy ↦ by_contra fun hne ↦ disjoint_left.1 (h hne) hx hy⟩

Characterization of Pairwise Disjoint Sets via Singleton Fibers

Informal description

For any family of sets $\{f_i\}_{i \in \iota}$ indexed by $\iota$, the following are equivalent: 1. For every element $a$, the set $\{i \in \iota \mid a \in f_i\}$ has at most one element. 2. The family $\{f_i\}_{i \in \iota}$ is pairwise disjoint under the relation $\text{Disjoint}$. Here, two sets $f_i$ and $f_j$ are called *disjoint* if their intersection is empty.

Mathlib.Data.Set.Pairwise.Basic

Main declarations

Notes