mathlib documentation

logic.relator

def relator.lift_fun {α : Sort u₁} {β : Sort u₂} {γ : Sort v₁} {δ : Sort v₂} :
(α → β → Prop)(γ → δ → Prop)(α → γ)(β → δ) → Prop

Equations
  • (R S) f g = ∀ ⦃a : α⦄ ⦃b : β⦄, R a bS (f a) (g b)
@[class]
def relator.right_total {α : Type u₁} {β : out_param (Type u₂)} :
out_param (α → β → Prop) → Prop

Equations
@[class]
def relator.left_total {α : Type u₁} {β : out_param (Type u₂)} :
out_param (α → β → Prop) → Prop

Equations
@[class]
def relator.bi_total {α : Type u₁} {β : out_param (Type u₂)} :
out_param (α → β → Prop) → Prop

Equations
Instances
@[class]
def relator.left_unique {α : Type u₁} {β : Type u₂} :
(α → β → Prop) → Prop

Equations
@[class]
def relator.right_unique {α : Type u₁} {β : Type u₂} :
(α → β → Prop) → Prop

Equations
theorem relator.rel_forall_of_right_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) [t : relator.right_total R] :
((R implies) implies) (λ (p : α → Prop), ∀ (i : α), p i) (λ (q : β → Prop), ∀ (i : β), q i)

theorem relator.rel_exists_of_left_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) [t : relator.left_total R] :
((R implies) implies) (λ (p : α → Prop), ∃ (i : α), p i) (λ (q : β → Prop), ∃ (i : β), q i)

theorem relator.rel_forall_of_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) [t : relator.bi_total R] :
((R iff) iff) (λ (p : α → Prop), ∀ (i : α), p i) (λ (q : β → Prop), ∀ (i : β), q i)

theorem relator.rel_exists_of_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) [t : relator.bi_total R] :
((R iff) iff) (λ (p : α → Prop), ∃ (i : α), p i) (λ (q : β → Prop), ∃ (i : β), q i)

theorem relator.left_unique_of_rel_eq {α : Type u₁} {β : Type u₂} (R : α → β → Prop) {eq' : β → β → Prop} :
(R R iff) eq eq'relator.left_unique R

@[instance]
def relator.bi_total_eq {α : Type u₁} :

def relator.bi_unique {α : Type u_1} {β : Type u_2} :
(α → β → Prop) → Prop

Equations
theorem relator.left_unique_flip {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :

theorem relator.rel_eq {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :