Relator for functions, pairs, sums, and lists. #
(R ⇒ S) f g
means LiftFun R S f g
.
Instances For
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)
:
theorem
Relator.LeftTotal.symm
{α : Type u_1}
{β : Type u_2}
{r₁₂ : α → β → Prop}
{r₂₁ : β → α → Prop}
(hr : (a : α) → (b : β) → r₁₂ a b → r₂₁ b a)
:
Relator.LeftTotal r₁₂ → Relator.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)
:
Relator.LeftTotal r₁₂ → Relator.LeftTotal r₂₃ → Relator.LeftTotal r₁₃
theorem
Relator.RightTotal.symm
{α : Type u_1}
{β : Type u_2}
{r₁₂ : α → β → Prop}
{r₂₁ : β → α → Prop}
(hr : (a : α) → (b : β) → r₁₂ a b → r₂₁ b a)
:
Relator.RightTotal r₁₂ → Relator.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)
:
Relator.RightTotal r₁₂ → Relator.RightTotal r₂₃ → Relator.RightTotal r₁₃
theorem
Relator.BiTotal.refl
{α : Type u_1}
{r₁₁ : α → α → Prop}
(hr : (a : α) → r₁₁ a a)
:
Relator.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)
:
Relator.BiTotal r₁₂ → Relator.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)
:
Relator.BiTotal r₁₂ → Relator.BiTotal r₂₃ → Relator.BiTotal r₁₃