mathlib docs: logic.relator

source

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

(α → β → Prop) → (γ → δ → Prop) → (α → γ) → (β → δ) → Prop

Equations

(R ⇒ S) f g = ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → S (f a) (g b)

source

@[class]

def relator.right_total {α : Type u₁} {β : out_param (Type u₂)} :

out_param (α → β → Prop) → Prop

Equations

relator.right_total R = ∀ (b : β), ∃ (a : α), R a b

source

@[class]

def relator.left_total {α : Type u₁} {β : out_param (Type u₂)} :

out_param (α → β → Prop) → Prop

Equations

relator.left_total R = ∀ (a : α), ∃ (b : β), R a b

source

@[class]

def relator.bi_total {α : Type u₁} {β : out_param (Type u₂)} :

out_param (α → β → Prop) → Prop

Equations

relator.bi_total R = (relator.left_total R ∧ relator.right_total R)

Instances

relator.bi_total_eq

source

@[class]

def relator.left_unique {α : Type u₁} {β : Type u₂} :

(α → β → Prop) → Prop

Equations

relator.left_unique R = ∀ {a : α} {b : β} {c : α}, R a b → R c b → a = c

source

@[class]

def relator.right_unique {α : Type u₁} {β : Type u₂} :

(α → β → Prop) → Prop

Equations

relator.right_unique R = ∀ {a : α} {b c : β}, R a b → R a c → b = c

source

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)

source

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)

source

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)

source

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)

source

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

(R ⇒ R ⇒ iff) eq eq' → relator.left_unique R

source

theorem relator.rel_imp :

(iff ⇒ iff ⇒ iff) implies implies

source

theorem relator.rel_not :

(iff ⇒ iff) not not

source

@[instance]

def relator.bi_total_eq {α : Type u₁} :

relator.bi_total eq

Equations

relator.bi_total_eq = _

source

def relator.bi_unique {α : Type u_1} {β : Type u_2} :

(α → β → Prop) → Prop

Equations

relator.bi_unique r = (relator.left_unique r ∧ relator.right_unique r)

source

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

relator.left_unique r → relator.right_unique (flip r)

source

theorem relator.rel_and :

(iff ⇒ iff ⇒ iff) and and

source

theorem relator.rel_or :

(iff ⇒ iff ⇒ iff) or or

source

theorem relator.rel_iff :

(iff ⇒ iff ⇒ iff) iff iff

source

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

relator.bi_unique r → (r ⇒ r ⇒ iff) eq eq

mathlib documentation

logic.relator

General documentation

Additional documentation

Library

mathlib documentation

logic.​relator

General documentation

Additional documentation

Library

logic.relator