logic.relator - mathlib docs

source

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

Prop

Equations

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

source

def relator.right_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :

Prop

Equations

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

source

def relator.left_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :

Prop

Equations

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

source

def relator.bi_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :

Prop

Equations

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

source

def relator.left_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :

Prop

Equations

relator.left_unique R = ∀ ⦃a b : α⦄ ⦃c : β⦄, R a c → R b c → a = b

source

def relator.right_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :

Prop

Equations

relator.right_unique R = ∀ ⦃a : α⦄ ⦃b c : β⦄, R a b → R a c → b = c

source

def relator.bi_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :

Prop

Equations

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

source

theorem relator.right_total.rel_forall {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : relator.right_total R) :

((R ⇒ implies) ⇒ implies) (λ (p : α → Prop), ∀ (i : α), p i) (λ (q : β → Prop), ∀ (i : β), q i)

source

theorem relator.left_total.rel_exists {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : relator.left_total R) :

((R ⇒ implies) ⇒ implies) (λ (p : α → Prop), ∃ (i : α), p i) (λ (q : β → Prop), ∃ (i : β), q i)

source

theorem relator.bi_total.rel_forall {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : relator.bi_total R) :

((R ⇒ iff) ⇒ iff) (λ (p : α → Prop), ∀ (i : α), p i) (λ (q : β → Prop), ∀ (i : β), q i)

source

theorem relator.bi_total.rel_exists {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : 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} (he : (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

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

relator.bi_total eq

source

theorem relator.left_unique.flip {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (h : 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} (hr : relator.bi_unique r) :

(r ⇒ r ⇒ iff) eq eq