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'.
(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))
A relation is "right total" if every element appears on the right.
Equations
- Relator.RightTotal R = ∀ (b : β), ∃ a, R a b
A relation is "left total" if every element appears on the left.
Equations
- Relator.LeftTotal R = ∀ (a : α), ∃ b, R a b
A relation is "bi-total" if it is both right total and left total.
Equations
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
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
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 => x → x_1) ⇒ fun x x_1 => x → x_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 => x → x_1) ⇒ fun x x_1 => x → x_1) (fun p => ∃ i, p i) fun q => ∃ i, q i
theorem
Relator.LeftUnique.flip
{α : Type u_1}
{β : Type u_2}
{r : α → β → Prop}
(h : Relator.LeftUnique r)
: