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)
@[class]
structure relator.right_total {α : Type u₁} {β : out_param (Type u₂)} (R : out_param (α → β → Prop)) :
Prop
  • right : ∀ (b : β), ∃ (a : α), R a b
Instances
@[class]
structure relator.left_total {α : Type u₁} {β : out_param (Type u₂)} (R : out_param (α → β → Prop)) :
Prop
  • left : ∀ (a : α), ∃ (b : β), R a b
Instances
@[class]
structure relator.bi_total {α : Type u₁} {β : out_param (Type u₂)} (R : out_param (α → β → Prop)) :
Prop
Instances
@[class]
structure relator.left_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
  • left : ∀ {a : α} {b : β} {c : α}, R a bR c ba = c
Instances
@[class]
structure relator.right_unique {α : Type u₁} {β : Type u₂} (R : α → β → Prop) :
Prop
  • right : ∀ {a : α} {b c : β}, R a bR a cb = c
Instances
theorem relator.left_unique.unique {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : relator.left_unique R) {a : α} {b : β} {c : α} :
R a bR c ba = c
theorem relator.right_unique.unique {α : Type u₁} {β : Type u₂} {R : α → β → Prop} (h : relator.right_unique R) {a : α} {b c : β} :
R a bR a cb = c
theorem relator.rel_forall_of_right_total {α : Type u₁} {β : Type u₂} (R : α → β → Prop) [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) [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) [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) [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') :
@[instance]
def relator.bi_total_eq {α : Type u₁} :
@[class]
structure relator.bi_unique {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :
Prop
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} (hr : relator.bi_unique r) :
(r r iff) eq eq