mathlib documentation

logic.relator

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 bS (f a) (g b)
def relator.right_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
def relator.left_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
def relator.bi_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
def relator.left_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
def relator.right_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
def relator.bi_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
Equations
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)
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)
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)
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)
theorem relator.left_unique_of_rel_eq {α : Type u₁} {β : Type u₂} {R : α → β → Prop} {eq' : β → β → Prop} (he : (R R iff) eq eq') :
theorem relator.bi_total_eq {α : Type u₁} :
theorem relator.left_unique.flip {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (h : relator.left_unique r) :
theorem relator.rel_eq {α : Type u_1} {β : Type u_2} {r : α → β → Prop} (hr : relator.bi_unique r) :
(r r iff) eq eq