mathlib3 documentation

logic.relator

Relator for functions, pairs, sums, and lists. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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
source
def relator.left_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
source
def relator.bi_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
source
def relator.left_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
source
def relator.right_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
source
def relator.bi_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
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