Relator for functions, pairs, sums, and lists.

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

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

Equations

• Relator.LiftFun R S f g = ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → S (f a) (g b)

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

(R ⇒ 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))

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

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

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)

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

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

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)

theorem Relator.RightTotal.rel_forall {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : RightTotal R) : LiftFun (LiftFun R fun (x1 : Sort u_1) (x2 : Prop) => x1 → x2) (fun (x1 : Sort (imax (u₁ + 1) u_1)) (x2 : Prop) => x1 → x2) (fun (p : α → Sort u_1) => (i : α) → p i) fun (q : β → Prop) => ∀ (i : β), q i

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

theorem Relator.BiTotal.rel_forall {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : BiTotal R) : LiftFun (LiftFun R Iff) Iff (fun (p : α → Prop) => ∀ (i : α), p i) fun (q : β → Prop) => ∀ (i : β), q i

theorem Relator.BiTotal.rel_exists {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : BiTotal R) : LiftFun (LiftFun R Iff) Iff (fun (p : α → Prop) => ∃ (i : α), p i) fun (q : β → Prop) => ∃ (i : β), q i

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

theorem Relator.rel_imp : LiftFun Iff (LiftFun Iff Iff) (fun (x1 x2 : Prop) => x1 → x2) fun (x1 x2 : Prop) => x1 → x2

theorem Relator.rel_not : LiftFun Iff Iff Not Not

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

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

theorem Relator.rel_and : LiftFun (fun (x1 x2 : Prop) => x1 ↔ x2) (LiftFun (fun (x1 x2 : Prop) => x1 ↔ x2) fun (x1 x2 : Prop) => x1 ↔ x2) (fun (x1 x2 : Prop) => x1 ∧ x2) fun (x1 x2 : Prop) => x1 ∧ x2

theorem Relator.rel_or : LiftFun (fun (x1 x2 : Prop) => x1 ↔ x2) (LiftFun (fun (x1 x2 : Prop) => x1 ↔ x2) fun (x1 x2 : Prop) => x1 ↔ x2) (fun (x1 x2 : Prop) => x1 ∨ x2) fun (x1 x2 : Prop) => x1 ∨ x2

theorem Relator.rel_iff : LiftFun (fun (x1 x2 : Prop) => x1 ↔ x2) (LiftFun (fun (x1 x2 : Prop) => x1 ↔ x2) fun (x1 x2 : Prop) => x1 ↔ x2) (fun (x1 x2 : Prop) => x1 ↔ x2) fun (x1 x2 : Prop) => x1 ↔ x2

theorem Relator.rel_eq {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : BiUnique r) : LiftFun r (LiftFun r fun (x1 x2 : Prop) => x1 ↔ x2) (fun (x1 x2 : α) => x1 = x2) fun (x1 x2 : β) => x1 = x2

theorem Relator.LeftTotal.refl {α : Type u_1} {r₁₁ : α → α → Prop} (hr : ∀ (a : α), r₁₁ a a) : LeftTotal r₁₁

theorem Relator.LeftTotal.symm {α : Type u_1} {β : Type u_2} {r₁₂ : α → β → Prop} {r₂₁ : β → α → Prop} (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : LeftTotal r₁₂ → RightTotal r₂₁

theorem Relator.LeftTotal.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r₁₂ : α → β → Prop} {r₂₃ : β → γ → Prop} {r₁₃ : α → γ → Prop} (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) : LeftTotal r₁₂ → LeftTotal r₂₃ → LeftTotal r₁₃

theorem Relator.RightTotal.refl {α : Type u_1} {r₁₁ : α → α → Prop} (hr : ∀ (a : α), r₁₁ a a) : RightTotal r₁₁

theorem Relator.RightTotal.symm {α : Type u_1} {β : Type u_2} {r₁₂ : α → β → Prop} {r₂₁ : β → α → Prop} (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : RightTotal r₁₂ → LeftTotal r₂₁

theorem Relator.RightTotal.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r₁₂ : α → β → Prop} {r₂₃ : β → γ → Prop} {r₁₃ : α → γ → Prop} (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) : RightTotal r₁₂ → RightTotal r₂₃ → RightTotal r₁₃

theorem Relator.BiTotal.refl {α : Type u_1} {r₁₁ : α → α → Prop} (hr : ∀ (a : α), r₁₁ a a) : BiTotal r₁₁

theorem Relator.BiTotal.symm {α : Type u_1} {β : Type u_2} {r₁₂ : α → β → Prop} {r₂₁ : β → α → Prop} (hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a) : BiTotal r₁₂ → BiTotal r₂₁

theorem Relator.BiTotal.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r₁₂ : α → β → Prop} {r₂₃ : β → γ → Prop} {r₁₃ : α → γ → Prop} (hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c) : BiTotal r₁₂ → BiTotal r₂₃ → BiTotal r₁₃