Mathlib.Logic.Pairwise

Pairwise definition

(r : α → α → Prop)

Full source

/-- A relation `r` holds pairwise if `r i j` for all `i ≠ j`. -/
def Pairwise (r : α → α → Prop) :=
  ∀ ⦃i j⦄, i ≠ j → r i j

Pairwise relation

Informal description

A relation $ r $ on a type $ \alpha $ is called *pairwise* if for any two distinct elements $ i $ and $ j $ in $ \alpha $, the relation $ r(i, j) $ holds. In other words, $ r $ holds between every pair of distinct elements in $ \alpha $.

Pairwise.mono theorem

(hr : Pairwise r) (h : ∀ ⦃i j⦄, r i j → p i j) : Pairwise p

Full source

theorem Pairwise.mono (hr : Pairwise r) (h : ∀ ⦃i j⦄, r i j → p i j) : Pairwise p :=
  fun _i _j hij => h <| hr hij

Pairwise Relation Implication: $ r \Rightarrow p $

Informal description

Let $ r $ and $ p $ be relations on a type $ \alpha $. If $ r $ holds pairwise on $ \alpha $ and for any two distinct elements $ i $ and $ j $ in $ \alpha $, $ r(i, j) $ implies $ p(i, j) $, then $ p $ also holds pairwise on $ \alpha $.

Pairwise.eq theorem

(h : Pairwise r) : ¬r a b → a = b

Full source

protected theorem Pairwise.eq (h : Pairwise r) : ¬r a b → a = b :=
  not_imp_comm.1 <| @h _ _

Equality from Negated Pairwise Relation: $\neg r(a, b) \Rightarrow a = b$

Informal description

Given a pairwise relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, if $r(a, b)$ does not hold, then $a = b$.

Subsingleton.pairwise theorem

[Subsingleton α] : Pairwise r

Full source

protected lemma Subsingleton.pairwise [Subsingleton α] : Pairwise r :=
  fun _ _ h ↦ False.elim <| h.elim <| Subsingleton.elim _ _

Pairwise Relation Holds for Subsingleton Types

Informal description

For any type $\alpha$ with at most one element (i.e., a subsingleton) and any relation $r$ on $\alpha$, the relation $r$ holds pairwise.

Function.injective_iff_pairwise_ne theorem

: Injective f ↔ Pairwise ((· ≠ ·) on f)

Full source

theorem Function.injective_iff_pairwise_ne : InjectiveInjective f ↔ Pairwise ((· ≠ ·) on f) :=
  forall₂_congr fun _i _j => not_imp_not.symm

Injectivity Criterion via Pairwise Inequality on Function Images

Informal description

A function $f \colon \alpha \to \beta$ is injective if and only if the relation $\neq$ (not equal) holds pairwise on the image of $f$, meaning that for any two distinct elements $x, y \in \alpha$, $f(x) \neq f(y)$.

Pairwise.comp_of_injective theorem

(hr : Pairwise r) {f : β → α} (hf : Injective f) : Pairwise (r on f)

Full source

lemma Pairwise.comp_of_injective (hr : Pairwise r) {f : β → α} (hf : Injective f) :
    Pairwise (r on f) :=
  fun _ _ h ↦ hr <| hf.ne h

Pairwise Relation Preserved Under Composition with Injective Function

Informal description

Let $r$ be a pairwise relation on a type $\alpha$, and let $f : \beta \to \alpha$ be an injective function. Then the relation $r$ composed with $f$, defined by $(r \text{ on } f)(x, y) = r(f(x), f(y))$ for $x, y \in \beta$, is also pairwise on $\beta$.

Pairwise.of_comp_of_surjective theorem

{f : β → α} (hr : Pairwise (r on f)) (hf : Surjective f) : Pairwise r

Full source

lemma Pairwise.of_comp_of_surjective {f : β → α} (hr : Pairwise (r on f)) (hf : Surjective f) :
    Pairwise r := hf.forall₂.2 fun _ _ h ↦ hr <| ne_of_apply_ne f h

Lifting Pairwise Relations via Surjective Functions

Informal description

Let $f \colon \beta \to \alpha$ be a surjective function. If the relation $r$ holds pairwise on the composition $r \circ f$ (i.e., for all distinct $x, y \in \beta$, $r(f(x), f(y))$ holds), then $r$ holds pairwise on $\alpha$ (i.e., for all distinct $a, b \in \alpha$, $r(a, b)$ holds).

Function.Bijective.pairwise_comp_iff theorem

{f : β → α} (hf : Bijective f) : Pairwise (r on f) ↔ Pairwise r

Full source

lemma Function.Bijective.pairwise_comp_iff {f : β → α} (hf : Bijective f) :
    PairwisePairwise (r on f) ↔ Pairwise r :=
  ⟨fun hr ↦ hr.of_comp_of_surjective hf.surjective, fun hr ↦ hr.comp_of_injective hf.injective⟩

Bijective Function Preserves Pairwise Relations via Composition

Informal description

Let $f \colon \beta \to \alpha$ be a bijective function. Then the relation $r$ holds pairwise on the composition $r \circ f$ (i.e., for all distinct $x, y \in \beta$, $r(f(x), f(y))$ holds) if and only if $r$ holds pairwise on $\alpha$ (i.e., for all distinct $a, b \in \alpha$, $r(a, b)$ holds).

Set.Pairwise definition

(s : Set α) (r : α → α → Prop)

Full source

/-- The relation `r` holds pairwise on the set `s` if `r x y` for all *distinct* `x y ∈ s`. -/
protected def Pairwise (s : Set α) (r : α → α → Prop) :=
  ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → x ≠ y → r x y

Pairwise relation on a set

Informal description

A set $s$ in a type $\alpha$ is said to satisfy the relation $r$ *pairwise* if for any two distinct elements $x, y \in s$, the relation $r(x, y)$ holds.

Set.pairwise_of_forall theorem

(s : Set α) (r : α → α → Prop) (h : ∀ a b, r a b) : s.Pairwise r

Full source

theorem pairwise_of_forall (s : Set α) (r : α → α → Prop) (h : ∀ a b, r a b) : s.Pairwise r :=
  fun a _ b _ _ => h a b

Universal Relation Implies Pairwise Relation on Any Set

Informal description

For any set $s$ in a type $\alpha$ and any binary relation $r$ on $\alpha$, if $r(a, b)$ holds for all $a, b \in \alpha$, then $s$ satisfies $r$ pairwise.

Set.Pairwise.imp_on theorem

(h : s.Pairwise r) (hrp : s.Pairwise fun ⦃a b : α⦄ => r a b → p a b) : s.Pairwise p

Full source

theorem Pairwise.imp_on (h : s.Pairwise r) (hrp : s.Pairwise fun ⦃a b : α⦄ => r a b → p a b) :
    s.Pairwise p :=
  fun _a ha _b hb hab => hrp ha hb hab <| h ha hb hab

Pairwise Relation Implication on a Set

Informal description

Let $s$ be a set in a type $\alpha$, and let $r$ and $p$ be binary relations on $\alpha$. If $s$ satisfies $r$ pairwise, and for any two distinct elements $a, b \in s$, the relation $r(a, b)$ implies $p(a, b)$, then $s$ satisfies $p$ pairwise.

Set.Pairwise.imp theorem

(h : s.Pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a b) : s.Pairwise p

Full source

theorem Pairwise.imp (h : s.Pairwise r) (hpq : ∀ ⦃a b : α⦄, r a b → p a b) : s.Pairwise p :=
  h.imp_on <| pairwise_of_forall s _ hpq

Pairwise Relation Implication Under Universal Condition

Informal description

Let $s$ be a set in a type $\alpha$, and let $r$ and $p$ be binary relations on $\alpha$. If $s$ satisfies $r$ pairwise and for any two distinct elements $a, b \in \alpha$, the relation $r(a, b)$ implies $p(a, b)$, then $s$ satisfies $p$ pairwise.

Set.Pairwise.eq theorem

(hs : s.Pairwise r) (ha : a ∈ s) (hb : b ∈ s) (h : ¬r a b) : a = b

Full source

protected theorem Pairwise.eq (hs : s.Pairwise r) (ha : a ∈ s) (hb : b ∈ s) (h : ¬r a b) : a = b :=
  of_not_not fun hab => h <| hs ha hb hab

Equality from Pairwise Relation and Non-Relation

Informal description

Let $s$ be a set in a type $\alpha$ and $r$ a relation on $\alpha$. If $r$ holds pairwise on $s$ (i.e., $r(x,y)$ for all distinct $x, y \in s$), and $a, b \in s$ are elements such that $\neg r(a, b)$, then $a = b$.

Reflexive.set_pairwise_iff theorem

(hr : Reflexive r) : s.Pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b

Full source

theorem _root_.Reflexive.set_pairwise_iff (hr : Reflexive r) :
    s.Pairwise r ↔ ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → r a b :=
  forall₄_congr fun a _ _ _ => or_iff_not_imp_left.symm.trans <| or_iff_right_of_imp <| Eq.ndrec <|
    hr a

Equivalence of Pairwise Relation and Universal Relation for Reflexive Relations on a Set

Informal description

Let $r$ be a reflexive relation on a type $\alpha$ (i.e., $r(x,x)$ holds for all $x \in \alpha$). For any subset $s \subseteq \alpha$, the following are equivalent: 1. The relation $r$ holds pairwise on $s$ (i.e., $r(x,y)$ for all distinct $x, y \in s$). 2. For all $x \in s$ and $y \in s$, the relation $r(x,y)$ holds.

Set.Pairwise.on_injective theorem

(hs : s.Pairwise r) (hf : Function.Injective f) (hfs : ∀ x, f x ∈ s) : Pairwise (r on f)

Full source

theorem Pairwise.on_injective (hs : s.Pairwise r) (hf : Function.Injective f) (hfs : ∀ x, f x ∈ s) :
    Pairwise (r on f) := fun i j hij => hs (hfs i) (hfs j) (hf.ne hij)

Pairwise Relation Preservation under Injective Functions

Informal description

Let $s$ be a set in a type $\alpha$ and $r$ a relation on $\alpha$. If $r$ holds pairwise on $s$ (i.e., $r(x,y)$ for all distinct $x, y \in s$), and $f$ is an injective function such that $f(x) \in s$ for all $x$ in its domain, then the relation $(r \text{ on } f)$ holds pairwise on the entire type. Here, $(r \text{ on } f)(x,y) := r(f(x), f(y))$.

Pairwise.set_pairwise theorem

(h : Pairwise r) (s : Set α) : s.Pairwise r

Full source

theorem Pairwise.set_pairwise (h : Pairwise r) (s : Set α) : s.Pairwise r := fun _ _ _ _ w => h w

Pairwise Relation Restricts to Subsets

Informal description

If a relation $r$ on a type $\alpha$ holds pairwise (i.e., $r(i,j)$ holds for all distinct $i,j \in \alpha$), then for any subset $s \subseteq \alpha$, the relation $r$ also holds pairwise on $s$.

Main declarations