Relator for functions, pairs, sums, and lists.

ink

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

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 b → S (f a) (g b))

ink

def Relator.«term_⇒_» : Lean.TrailingParserDescr

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

Equations

• Relator.«term_⇒_» = Lean.ParserDescr.trailingNode `Relator.term_⇒_ 40 41 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇒ ") (Lean.ParserDescr.cat `term 40))

ink

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

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

Equations

• Relator.RightTotal R = ∀ (b : β), ∃ a, R a b

ink

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

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

Equations

• Relator.LeftTotal R = ∀ (a : α), ∃ b, R a b

ink

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

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

Equations

• Relator.BiTotal R = (Relator.LeftTotal R ∧ Relator.RightTotal R)

ink

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

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

Equations

• Relator.LeftUnique R = ∀ ⦃a b : α⦄ ⦃c : β⦄, R a c → R b c → a = b

ink

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

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

Equations

• Relator.RightUnique R = ∀ ⦃a : α⦄ ⦃b c : β⦄, R a b → R a c → b = c

ink

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

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

Equations

• Relator.BiUnique R = (Relator.LeftUnique R ∧ Relator.RightUnique R)

ink

theorem Relator.RightTotal.rel_forall {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : Relator.RightTotal R) : ((R ⇒ fun x x_1 => x → x_1) ⇒ fun x x_1 => x → x_1) (fun p => (i : α) → p i) fun q => ∀ (i : β), q i

ink

theorem Relator.LeftTotal.rel_exists {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : Relator.LeftTotal R) : ((R ⇒ fun x x_1 => x → x_1) ⇒ fun x x_1 => x → x_1) (fun p => ∃ i, p i) fun q => ∃ i, q i

ink

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

ink

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

ink

theorem Relator.left_unique_of_rel_eq {α : Type u₁} {β : Type u₂} {R : α → β → Prop} {eq' : β → β → Prop} (he : (R ⇒ R ⇒ Iff) Eq eq') : Relator.LeftUnique R

ink

theorem Relator.rel_imp : (Iff ⇒ Iff ⇒ Iff) (fun x x_1 => x → x_1) fun x x_1 => x → x_1

ink

theorem Relator.rel_not : (Iff ⇒ Iff) Not Not

ink

theorem Relator.bi_total_eq {α : Type u₁} : Relator.BiTotal Eq

ink

theorem Relator.LeftUnique.flip {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (h : Relator.LeftUnique r) : Relator.RightUnique (flip r)

ink

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

ink

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

ink

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

ink

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