Documentation

Mathlib.Logic.Relator

Relator for functions, pairs, sums, and lists. #

def Relator.LiftFun {α : Sort u₁} {β : Sort u₂} {γ : Sort v₁} {δ : Sort v₂} (R : αβProp) (S : γδProp) (f : αγ) (g : βδ) :

The binary relations R : α → β → Prop→ β → Prop→ Prop and S : γ → δ → Prop→ δ → Prop→ Prop induce a binary relation on functions `LiftFun : (f : α → γ) (g : β → δ) : Prop'.

Equations
  • (R S) f g = (a : α⦄ → b : β⦄ → R a bS (f a) (g b))

(R ⇒ S) f g⇒ S) f g means LiftFun R S f g.

Equations
def Relator.RightTotal {α : Type u₁} {β : Type u₂} (R : αβProp) :

A relation is "right total" if every element appears on the right.

Equations
def Relator.LeftTotal {α : Type u₁} {β : Type u₂} (R : αβProp) :

A relation is "left total" if every element appears on the left.

Equations
def Relator.BiTotal {α : Type u₁} {β : Type u₂} (R : αβProp) :

A relation is "bi-total" if it is both right total and left total.

Equations
def Relator.LeftUnique {α : Type u₁} {β : Type u₂} (R : αβProp) :

A relation is "left unique" if every element on the right is paired with at most one element on the left.

Equations
def Relator.RightUnique {α : Type u₁} {β : Type u₂} (R : αβProp) :

A relation is "right unique" if every element on the left is paired with at most one element on the right.

Equations
def Relator.BiUnique {α : Type u₁} {β : Type u₂} (R : αβProp) :

A relation is "bi-unique" if it is both left unique and right unique.

Equations
theorem Relator.RightTotal.rel_forall {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.RightTotal R) :
((R fun x x_1 => xx_1) fun x x_1 => xx_1) (fun p => (i : α) → p i) fun q => ∀ (i : β), q i
theorem Relator.LeftTotal.rel_exists {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.LeftTotal R) :
((R fun x x_1 => xx_1) fun x x_1 => xx_1) (fun p => i, p i) fun q => i, q i
theorem Relator.BiTotal.rel_forall {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.BiTotal R) :
((R Iff) Iff) (fun p => ∀ (i : α), p i) fun q => ∀ (i : β), q i
theorem Relator.BiTotal.rel_exists {α : Type u₁} {β : Type u₂} {R : αβProp} (h : Relator.BiTotal R) :
((R Iff) Iff) (fun p => i, p i) fun q => i, q i
theorem Relator.left_unique_of_rel_eq {α : Type u₁} {β : Type u₂} {R : αβProp} {eq' : ββProp} (he : (R R Iff) Eq eq') :
theorem Relator.rel_imp :
(Iff Iff Iff) (fun x x_1 => xx_1) fun x x_1 => xx_1
theorem Relator.LeftUnique.flip {α : Type u_1} {β : Type u_2} {r : αβProp} (h : Relator.LeftUnique r) :
theorem Relator.rel_and :
((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
theorem Relator.rel_or :
((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
theorem Relator.rel_iff :
((fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1) (fun x x_1 => x x_1) fun x x_1 => x x_1
theorem Relator.rel_eq {α : Type u_1} {β : Type u_2} {r : αβProp} (hr : Relator.BiUnique r) :
(r r fun x x_1 => x x_1) (fun x x_1 => x = x_1) fun x x_1 => x = x_1