Mathlib.Logic.Relator

Relator.LiftFun definition

(f : α → γ) (g : β → δ) : Prop

Full source

/-- The binary relations `R : α → β → Prop` and `S : γ → δ → Prop` induce a binary
    relation on functions `LiftFun : (α → γ) → (β → δ) → Prop`. -/
def LiftFun (f : α → γ) (g : β → δ) : Prop :=
  ∀⦃a b⦄, R a b → S (f a) (g b)

Lifted function relation

Informal description

Given binary relations $R : \alpha \to \beta \to \text{Prop}$ and $S : \gamma \to \delta \to \text{Prop}$, the relation $\text{LiftFun}(f, g)$ holds for functions $f : \alpha \to \gamma$ and $g : \beta \to \delta$ if for all $a \in \alpha$ and $b \in \beta$ such that $R(a, b)$, we have $S(f(a), g(b))$.

Relator.term_⇒_ definition

: Lean.TrailingParserDescr✝

Full source

/-- `(R ⇒ S) f g` means `LiftFun R S f g`. -/
scoped infixr:40 " ⇒ " => LiftFun

Function relation notation `R ⇒ S`

Informal description

The notation `(R ⇒ S) f g` is defined to mean `LiftFun R S f g`, where `LiftFun` is a relation between functions `f : α → γ` and `g : β → δ` with respect to relations `R` on `α × β` and `S` on `γ × δ`.

Relator.RightTotal definition

: Prop

Full source

/-- A relation is "right total" if every element appears on the right. -/
def RightTotal : Prop := ∀ b, ∃ a, R a b

Right total relation

Informal description

A relation $R$ on a type is called *right total* if for every element $b$ in the codomain, there exists an element $a$ in the domain such that $R(a, b)$ holds.

Relator.LeftTotal definition

: Prop

Full source

/-- A relation is "left total" if every element appears on the left. -/
def LeftTotal : Prop := ∀ a, ∃ b, R a b

Left total relation

Informal description

A relation $R$ is called *left total* if for every element $a$ in the domain, there exists an element $b$ in the codomain such that $R(a, b)$ holds. In other words, every element on the left is related to at least one element on the right.

Relator.BiTotal definition

: Prop

Full source

/-- A relation is "bi-total" if it is both right total and left total. -/
def BiTotal : Prop := LeftTotalLeftTotal R ∧ RightTotal R

Bi-total relation

Informal description

A relation $R$ is called *bi-total* if it is both left total and right total. That is, for every element $a$ in the domain, there exists an element $b$ in the codomain such that $R(a, b)$ holds (left total), and for every element $b$ in the codomain, there exists an element $a$ in the domain such that $R(a, b)$ holds (right total).

Relator.LeftUnique definition

: Prop

Full source

/-- A relation is "left unique" if every element on the right is paired with at
    most one element on the left. -/
def LeftUnique : Prop := ∀ ⦃a b c⦄, R a c → R b c → a = b

Left unique relation

Informal description

A relation $R$ is called *left unique* if for any elements $a$, $b$, and $c$, whenever $R(a, c)$ and $R(b, c)$ hold, it follows that $a = b$. In other words, each element on the right is related to at most one element on the left.

Relator.RightUnique definition

: Prop

Full source

/-- A relation is "right unique" if every element on the left is paired with at
    most one element on the right. -/
def RightUnique : Prop := ∀ ⦃a b c⦄, R a b → R a c → b = c

Right unique relation

Informal description

A relation $R$ is called right unique if for any elements $a$, $b$, and $c$, whenever $R$ relates $a$ to $b$ and $a$ to $c$, then $b$ must equal $c$. In other words, each element on the left is related to at most one element on the right.

Relator.BiUnique definition

: Prop

Full source

/-- A relation is "bi-unique" if it is both left unique and right unique. -/
def BiUnique : Prop := LeftUniqueLeftUnique R ∧ RightUnique R

Bi-unique relation

Informal description

A relation $R$ is called *bi-unique* if it is both left unique and right unique. That is: 1. (Left unique) For any elements $a$, $b$, and $c$, if $R(a, c)$ and $R(b, c)$ hold, then $a = b$. 2. (Right unique) For any elements $a$, $b$, and $c$, if $R(a, b)$ and $R(a, c)$ hold, then $b = c$.

Relator.RightTotal.rel_forall theorem

(h : RightTotal R) : ((R ⇒ (· → ·)) ⇒ (· → ·)) (fun p => ∀ i, p i) (fun q => ∀ i, q i)

Full source

lemma RightTotal.rel_forall (h : RightTotal R) :
    ((R ⇒ (· → ·)) ⇒ (· → ·)) (fun p => ∀i, p i) (fun q => ∀i, q i) :=
  fun _ _ Hrel H b => Exists.elim (h b) (fun _ Rab => Hrel Rab (H _))

Right Total Relation Preserves Universal Quantification

Informal description

Let $R$ be a right total relation. Then for any pair of predicates $p$ and $q$ such that $R$ implies a functional relation between them (i.e., $R \Rightarrow (\cdot \rightarrow \cdot)$), the universal quantification over $p$ implies the universal quantification over $q$. In other words, if for all $i$, $p(i)$ holds, then for all $i$, $q(i)$ holds under the assumption that $R$ is right total and functionally relates $p$ to $q$.

Relator.LeftTotal.rel_exists theorem

(h : LeftTotal R) : ((R ⇒ (· → ·)) ⇒ (· → ·)) (fun p => ∃ i, p i) (fun q => ∃ i, q i)

Full source

lemma LeftTotal.rel_exists (h : LeftTotal R) :
    ((R ⇒ (· → ·)) ⇒ (· → ·)) (fun p => ∃i, p i) (fun q => ∃i, q i) :=
  fun _ _ Hrel ⟨a, pa⟩ => (h a).imp fun _ Rab => Hrel Rab pa

Existential Quantifier Preservation under Left Total Relations

Informal description

Let $R$ be a left total relation. Then for any predicates $p$ and $q$ such that $R$ lifts to an implication between $p$ and $q$ (i.e., for all $a$ and $b$ with $R(a, b)$, we have $p(a) \to q(b)$), the existential quantification over $p$ implies the existential quantification over $q$. In other words, if there exists some $i$ such that $p(i)$ holds, then there exists some $i$ such that $q(i)$ holds.

Relator.BiTotal.rel_forall theorem

(h : BiTotal R) : ((R ⇒ Iff) ⇒ Iff) (fun p => ∀ i, p i) (fun q => ∀ i, q i)

Full source

lemma BiTotal.rel_forall (h : BiTotal R) :
    ((R ⇒ Iff) ⇒ Iff) (fun p => ∀i, p i) (fun q => ∀i, q i) :=
  fun _ _ Hrel =>
    ⟨fun H b => Exists.elim (h.right b) (fun _ Rab => (Hrel Rab).mp (H _)),
      fun H a => Exists.elim (h.left a) (fun _ Rab => (Hrel Rab).mpr (H _))⟩

Universal Quantifier Equivalence under Bi-total Relations

Informal description

Let $R$ be a bi-total relation. Then for any pair of predicates $p$ and $q$ such that $R$ implies a bidirectional implication between them (i.e., $R \Rightarrow \text{Iff}$), the universal quantification over $p$ is equivalent to the universal quantification over $q$. In other words, for all $i$, $p(i)$ holds if and only if for all $i$, $q(i)$ holds.

Relator.BiTotal.rel_exists theorem

(h : BiTotal R) : ((R ⇒ Iff) ⇒ Iff) (fun p => ∃ i, p i) (fun q => ∃ i, q i)

Full source

lemma BiTotal.rel_exists (h : BiTotal R) :
    ((R ⇒ Iff) ⇒ Iff) (fun p => ∃i, p i) (fun q => ∃i, q i) :=
  fun _ _ Hrel =>
    ⟨fun ⟨a, pa⟩ => (h.left a).imp fun _ Rab => (Hrel Rab).1 pa,
      fun ⟨b, qb⟩ => (h.right b).imp fun _ Rab => (Hrel Rab).2 qb⟩

Existential Quantifier Equivalence under Bi-total Relations

Informal description

Let $R$ be a bi-total relation. Then for any pair of predicates $p$ and $q$ such that $R$ implies a bidirectional implication between them (i.e., $R(a, b) \Rightarrow (p(a) \leftrightarrow q(b))$ for all $a, b$), the existential quantification over $p$ is equivalent to the existential quantification over $q$. In other words, there exists some $i$ such that $p(i)$ holds if and only if there exists some $i$ such that $q(i)$ holds.

Relator.left_unique_of_rel_eq theorem

{eq' : β → β → Prop} (he : (R ⇒ (R ⇒ Iff)) Eq eq') : LeftUnique R

Full source

lemma left_unique_of_rel_eq {eq' : β → β → Prop} (he : (R ⇒ (R ⇒ Iff)) Eq eq') : LeftUnique R :=
  fun a b c (ac : R a c) (bc : R b c) => (he ac bc).mpr ((he bc bc).mp rfl)

Left Uniqueness from Relation Equivalence

Informal description

Let $R$ be a binary relation on a type $\beta$ and let $\text{eq}'$ be another binary relation on $\beta$. If for all $a, b \in \beta$, the relation $R(a, b)$ implies that $\text{Eq}(a, b) \leftrightarrow \text{eq}'(a, b)$, then $R$ is left unique. That is, for any $a, b, c \in \beta$, if $R(a, c)$ and $R(b, c)$ hold, then $a = b$.

Relator.rel_imp theorem

: (Iff ⇒ (Iff ⇒ Iff)) (· → ·) (· → ·)

Full source

lemma rel_imp : (IffIff ⇒ (Iff ⇒ Iff)) (· → ·) (· → ·) :=
  fun _ _ h _ _ l => imp_congr h l

Implication Preserves Logical Equivalence

Informal description

The relation `Relator.rel_imp` states that for any two propositions `P ↔ Q` and `P' ↔ Q'`, the implication `P → P'` holds if and only if the implication `Q → Q'` holds. In other words, implication preserves logical equivalence in both arguments.

Relator.rel_not theorem

: (Iff ⇒ Iff) Not Not

Full source

lemma rel_not : (IffIff ⇒ Iff) Not Not :=
  fun _ _ h => not_congr h

Negation Preserves Biconditional Relation

Informal description

The logical negation operation `Not` preserves the biconditional relation `Iff`, meaning that for any propositions `P` and `Q`, if `P ↔ Q` holds, then `¬P ↔ ¬Q` also holds.

Relator.bi_total_eq theorem

{α : Type u₁} : Relator.BiTotal (@Eq α)

Full source

lemma bi_total_eq {α : Type u₁} : Relator.BiTotal (@Eq α) :=
  { left := fun a => ⟨a, rfl⟩, right := fun a => ⟨a, rfl⟩ }

Equality is Bi-total on Any Type

Informal description

For any type $\alpha$, the equality relation $=$ on $\alpha$ is bi-total, meaning it is both left total and right total. That is, for every element $a \in \alpha$, there exists an element $b \in \alpha$ such that $a = b$ (left total), and for every element $b \in \alpha$, there exists an element $a \in \alpha$ such that $a = b$ (right total).

Relator.LeftUnique.flip theorem

(h : LeftUnique r) : RightUnique (flip r)

Full source

lemma LeftUnique.flip (h : LeftUnique r) : RightUnique (flip r) :=
  fun _ _ _ h₁ h₂ => h h₁ h₂

Flipping a left unique relation yields a right unique relation

Informal description

If a relation $r$ is left unique, then its flipped relation (where the arguments are reversed) is right unique.

Relator.rel_and theorem

: ((· ↔ ·) ⇒ (· ↔ ·) ⇒ (· ↔ ·)) (· ∧ ·) (· ∧ ·)

Full source

lemma rel_and : ((·↔·) ⇒ (·↔·) ⇒ (·↔·)) (·∧·) (·∧·) :=
  fun _ _ h₁ _ _ h₂ => and_congr h₁ h₂

Conjunction Preserves Lifted Function Relation

Informal description

Given binary relations $R_1 : \alpha \to \beta \to \text{Prop}$ and $R_2 : \gamma \to \delta \to \text{Prop}$, the conjunction operation $\land$ preserves the relation $\text{LiftFun}(R_1, R_2)$. That is, if $R_1(a, b)$ and $R_2(c, d)$ hold, then $(a \land c, b \land d) \in \text{LiftFun}(R_1, R_2)$.

Relator.rel_or theorem

: ((· ↔ ·) ⇒ (· ↔ ·) ⇒ (· ↔ ·)) (· ∨ ·) (· ∨ ·)

Full source

lemma rel_or : ((·↔·) ⇒ (·↔·) ⇒ (·↔·)) (·∨·) (·∨·) :=
  fun _ _ h₁ _ _ h₂ => or_congr h₁ h₂

Logical Or Preserved Under Function Relations

Informal description

Given binary relations $R_1, R_2 : \alpha \to \beta \to \text{Prop}$ and $S_1, S_2 : \gamma \to \delta \to \text{Prop}$, the relation $\text{rel\_or}$ holds for functions $f_1, f_2 : \alpha \to \gamma$ and $g_1, g_2 : \beta \to \delta$ if for all $a \in \alpha$ and $b \in \beta$, the following equivalence holds: $$(R_1(a, b) \lor R_2(a, b)) \leftrightarrow (S_1(f_1(a), g_1(b)) \lor S_2(f_2(a), g_2(b))).$$

Relator.rel_iff theorem

: ((· ↔ ·) ⇒ (· ↔ ·) ⇒ (· ↔ ·)) (· ↔ ·) (· ↔ ·)

Full source

lemma rel_iff : ((·↔·) ⇒ (·↔·) ⇒ (·↔·)) (·↔·) (·↔·) :=
  fun _ _ h₁ _ _ h₂ => iff_congr h₁ h₂

Logical Equivalence Preserved Under Function Relations

Informal description

Given binary relations $R_1, R_2 : \alpha \to \beta \to \text{Prop}$ and $S_1, S_2 : \gamma \to \delta \to \text{Prop}$, the relation $\text{rel\_iff}$ holds for functions $f_1, f_2 : \alpha \to \gamma$ and $g_1, g_2 : \beta \to \delta$ if for all $a \in \alpha$ and $b \in \beta$, the following equivalence holds: $$(R_1(a, b) \leftrightarrow R_2(a, b)) \leftrightarrow (S_1(f_1(a), g_1(b)) \leftrightarrow S_2(f_2(a), g_2(b))).$$

Relator.rel_eq theorem

{r : α → β → Prop} (hr : BiUnique r) : (r ⇒ r ⇒ (· ↔ ·)) (· = ·) (· = ·)

Full source

lemma rel_eq {r : α → β → Prop} (hr : BiUnique r) : (r ⇒ r ⇒ (·↔·)) (·=·) (·=·) :=
  fun _ _ h₁ _ _ h₂ => ⟨fun h => hr.right h₁ <| h.symm ▸ h₂, fun h => hr.left h₁ <| h.symm ▸ h₂⟩

Bi-unique Relations Preserve Equality

Informal description

For any bi-unique relation $r : \alpha \to \beta \to \text{Prop}$, the equality relation is preserved under $r$. That is, for any $a_1, a_2 \in \alpha$ and $b_1, b_2 \in \beta$ such that $r(a_1, b_1)$ and $r(a_2, b_2)$ hold, we have $a_1 = a_2 \leftrightarrow b_1 = b_2$.

Relator.LeftTotal.refl theorem

(hr : ∀ a : α, r₁₁ a a) : LeftTotal r₁₁

Full source

protected lemma refl (hr : ∀ a : α, r₁₁ a a) :
    LeftTotal r₁₁ :=
  fun a ↦ ⟨a, hr _⟩

Reflexivity Implies Left Totality

Informal description

For any relation $r_{11}$ on a type $\alpha$, if $r_{11}$ is reflexive (i.e., $r_{11}(a, a)$ holds for every $a \in \alpha$), then $r_{11}$ is left total.

Relator.LeftTotal.symm theorem

(hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : LeftTotal r₁₂ → RightTotal r₂₁

Full source

protected lemma symm (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) :
    LeftTotal r₁₂ → RightTotal r₂₁ :=
  fun h a ↦ (h a).imp (fun _ ↦ hr _ _)

Symmetry of Left and Right Total Relations

Informal description

Let $r_{12}$ be a relation between types $\alpha$ and $\beta$, and $r_{21}$ a relation between $\beta$ and $\alpha$. If for all $a \in \alpha$ and $b \in \beta$, $r_{12}(a, b)$ implies $r_{21}(b, a)$, then left totality of $r_{12}$ implies right totality of $r_{21}$.

Relator.LeftTotal.trans theorem

 (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) : LeftTotal r₁₂ → LeftTotal r₂₃ → LeftTotal r₁₃

Full source

protected lemma trans (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) :
    LeftTotal r₁₂ → LeftTotal r₂₃ → LeftTotal r₁₃ :=
  fun h₁ h₂ a ↦ let ⟨b, hab⟩ := h₁ a; let ⟨c, hbc⟩ := h₂ b; ⟨c, hr _ _ _ hab hbc⟩

Transitivity of Left Total Relations

Informal description

For any relations $r_{12} \subseteq \alpha \times \beta$, $r_{23} \subseteq \beta \times \gamma$, and $r_{13} \subseteq \alpha \times \gamma$, if: 1. For all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, whenever $r_{12}(a, b)$ and $r_{23}(b, c)$ hold, then $r_{13}(a, c)$ holds, 2. $r_{12}$ is left total (for every $a \in \alpha$ there exists $b \in \beta$ with $r_{12}(a, b)$), 3. $r_{23}$ is left total (for every $b \in \beta$ there exists $c \in \gamma$ with $r_{23}(b, c)$), then $r_{13}$ is left total (for every $a \in \alpha$ there exists $c \in \gamma$ with $r_{13}(a, c)$).

Relator.RightTotal.refl theorem

(hr : ∀ a : α, r₁₁ a a) : RightTotal r₁₁

Full source

protected lemma refl (hr : ∀ a : α, r₁₁ a a) : RightTotal r₁₁ :=
  LeftTotal.refl hr

Reflexivity Implies Right Totality

Informal description

For any reflexive relation $r_{11}$ on a type $\alpha$ (i.e., $r_{11}(a, a)$ holds for every $a \in \alpha$), the relation $r_{11}$ is right total (i.e., for every $a \in \alpha$, there exists $a' \in \alpha$ such that $r_{11}(a', a)$ holds).

Relator.RightTotal.symm theorem

(hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : RightTotal r₁₂ → LeftTotal r₂₁

Full source

protected lemma symm (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) :
    RightTotal r₁₂ → LeftTotal r₂₁ :=
  LeftTotal.symm (fun _ _ ↦ hr _ _)

Symmetry of Right and Left Total Relations

Informal description

Let $r_{12}$ be a relation between types $\alpha$ and $\beta$, and $r_{21}$ a relation between $\beta$ and $\alpha$. If for all $a \in \alpha$ and $b \in \beta$, $r_{12}(a, b)$ implies $r_{21}(b, a)$, then right totality of $r_{12}$ implies left totality of $r_{21}$.

Relator.RightTotal.trans theorem

 (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) : RightTotal r₁₂ → RightTotal r₂₃ → RightTotal r₁₃

Full source

protected lemma trans (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) :
    RightTotal r₁₂ → RightTotal r₂₃ → RightTotal r₁₃ :=
  swap <| LeftTotal.trans (fun _ _ _ ↦ swap <| hr _ _ _)

Transitivity of Right Total Relations

Informal description

For any relations $r_{12} \subseteq \alpha \times \beta$, $r_{23} \subseteq \beta \times \gamma$, and $r_{13} \subseteq \alpha \times \gamma$, if: 1. For all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, whenever $r_{12}(a, b)$ and $r_{23}(b, c)$ hold, then $r_{13}(a, c)$ holds, 2. $r_{12}$ is right total (for every $b \in \beta$ there exists $a \in \alpha$ with $r_{12}(a, b)$), 3. $r_{23}$ is right total (for every $c \in \gamma$ there exists $b \in \beta$ with $r_{23}(b, c)$), then $r_{13}$ is right total (for every $c \in \gamma$ there exists $a \in \alpha$ with $r_{13}(a, c)$).

Relator.BiTotal.refl theorem

(hr : ∀ a : α, r₁₁ a a) : BiTotal r₁₁

Full source

protected lemma refl (hr : ∀ a : α, r₁₁ a a) :
    BiTotal r₁₁ :=
  ⟨LeftTotal.refl hr, RightTotal.refl hr⟩

Reflexivity Implies Bi-totality

Informal description

For any reflexive relation $r_{11}$ on a type $\alpha$ (i.e., $r_{11}(a, a)$ holds for every $a \in \alpha$), the relation $r_{11}$ is bi-total (both left total and right total).

Relator.BiTotal.symm theorem

(hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : BiTotal r₁₂ → BiTotal r₂₁

Full source

protected lemma symm (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) :
    BiTotal r₁₂ → BiTotal r₂₁ :=
  fun h ↦ ⟨h.2.symm hr, h.1.symm hr⟩

Symmetry of Bi-total Relations

Informal description

Let $r_{12}$ be a relation between types $\alpha$ and $\beta$, and $r_{21}$ a relation between $\beta$ and $\alpha$. If for all $a \in \alpha$ and $b \in \beta$, $r_{12}(a, b)$ implies $r_{21}(b, a)$, then bi-totality of $r_{12}$ implies bi-totality of $r_{21}$.

Relator.BiTotal.trans theorem

 (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) : BiTotal r₁₂ → BiTotal r₂₃ → BiTotal r₁₃

Full source

protected lemma trans (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) :
    BiTotal r₁₂ → BiTotal r₂₃ → BiTotal r₁₃ :=
  fun h₁ h₂ ↦ ⟨h₁.1.trans hr h₂.1, h₁.2.trans hr h₂.2⟩

Transitivity of Bi-total Relations

Informal description

For any relations $r_{12} \subseteq \alpha \times \beta$, $r_{23} \subseteq \beta \times \gamma$, and $r_{13} \subseteq \alpha \times \gamma$, if: 1. For all $a \in \alpha$, $b \in \beta$, and $c \in \gamma$, whenever $r_{12}(a, b)$ and $r_{23}(b, c)$ hold, then $r_{13}(a, c)$ holds, 2. $r_{12}$ is bi-total (both left and right total), 3. $r_{23}$ is bi-total (both left and right total), then $r_{13}$ is bi-total (both left and right total).