# mathlibdocumentation

logic.relation

def relation.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} :
(α → β → Prop)(β → γ → Prop)α → γ → Prop

The composition of two relations, yielding a new relation. The result relates a term of α and a term of γ if there is an intermediate term of β related to both.

Equations
• a c = ∃ (b : β), r a b p b c
theorem relation.comp_eq {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
= r

theorem relation.eq_comp {α : Type u_1} {β : Type u_2} {r : α → β → Prop} :
= r

theorem relation.iff_comp {α : Type u_1} {r : Prop → α → Prop} :

theorem relation.comp_iff {α : Type u_1} {r : α → Prop → Prop} :

theorem relation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {r : α → β → Prop} {p : β → γ → Prop} {q : γ → δ → Prop} :
q = q)

theorem relation.flip_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} {r : α → β → Prop} {p : β → γ → Prop} :
flip p) = (flip r)

def relation.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} :
(α → β → Prop)(α → γ)(β → δ)γ → δ → Prop

The map of a relation r through a pair of functions pushes the relation to the codomains of the functions. The resulting relation is defined by having pairs of terms related if they have preimages related by r.

Equations
• f g = λ (c : γ) (d : δ), ∃ (a : α) (b : β), r a b f a = c g b = d
inductive relation.refl_trans_gen {α : Type u_1} :
(α → α → Prop)α → α → Prop
• refl : ∀ {α : Type u_1} (r : α → α → Prop) (a : α),
• tail : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b c : α}, r b c

refl_trans_gen r: reflexive transitive closure of r

inductive relation.refl_gen {α : Type u_1} :
(α → α → Prop)α → α → Prop
• refl : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), a
• single : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b : α}, r a b b

refl_gen r: reflexive closure of r

inductive relation.trans_gen {α : Type u_1} :
(α → α → Prop)α → α → Prop
• single : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b : α}, r a b b
• tail : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b c : α}, br b c c

trans_gen r: transitive closure of r

theorem relation.refl_gen.to_refl_trans_gen {α : Type u_1} {r : α → α → Prop} {a b : α} :
b

theorem relation.refl_trans_gen.trans {α : Type u_1} {r : α → α → Prop} {a b c : α} :

theorem relation.refl_trans_gen.single {α : Type u_1} {r : α → α → Prop} {a b : α} :
r a b

theorem relation.refl_trans_gen.head {α : Type u_1} {r : α → α → Prop} {a b c : α} :
r a b

theorem relation.refl_trans_gen.symmetric {α : Type u_1} {r : α → α → Prop} :

theorem relation.refl_trans_gen.cases_tail {α : Type u_1} {r : α → α → Prop} {a b : α} :
(b = a ∃ (c : α), r c b)

theorem relation.refl_trans_gen.head_induction_on {α : Type u_1} {r : α → α → Prop} {b : α} {P : Π (a : α), → Prop} {a : α} (h : b) :
(∀ {a c : α} (h' : r a c) (h : b), P c hP a _)P a h

theorem relation.refl_trans_gen.trans_induction_on {α : Type u_1} {r : α → α → Prop} {P : Π {a b : α}, → Prop} {a b : α} (h : b) :
(∀ (a : α), (∀ {a b : α} (h : r a b), P _)(∀ {a b c : α} (h₁ : b) (h₂ : c), P h₁P h₂P _)P h

theorem relation.refl_trans_gen.cases_head {α : Type u_1} {r : α → α → Prop} {a b : α} :
(a = b ∃ (c : α), r a c b)

theorem relation.refl_trans_gen.cases_head_iff {α : Type u_1} {r : α → α → Prop} {a b : α} :
a = b ∃ (c : α), r a c

theorem relation.refl_trans_gen.total_of_right_unique {α : Type u_1} {r : α → α → Prop} {a b c : α} :

theorem relation.trans_gen.to_refl {α : Type u_1} {r : α → α → Prop} {a b : α} :
b

theorem relation.trans_gen.trans_left {α : Type u_1} {r : α → α → Prop} {a b c : α} :
b c

theorem relation.trans_gen.trans {α : Type u_1} {r : α → α → Prop} {a b c : α} :
b c c

theorem relation.trans_gen.head' {α : Type u_1} {r : α → α → Prop} {a b c : α} :
r a b c

theorem relation.trans_gen.tail' {α : Type u_1} {r : α → α → Prop} {a b c : α} :
r b c c

theorem relation.trans_gen.trans_right {α : Type u_1} {r : α → α → Prop} {a b c : α} :
c c

theorem relation.trans_gen.head {α : Type u_1} {r : α → α → Prop} {a b c : α} :
r a b c c

theorem relation.trans_gen.tail'_iff {α : Type u_1} {r : α → α → Prop} {a c : α} :
c ∃ (b : α), r b c

theorem relation.trans_gen.head'_iff {α : Type u_1} {r : α → α → Prop} {a c : α} :
c ∃ (b : α), r a b

theorem relation.refl_trans_gen_iff_eq {α : Type u_1} {r : α → α → Prop} {a b : α} :
(∀ (b : α), ¬r a b) b b = a)

theorem relation.refl_trans_gen_iff_eq_or_trans_gen {α : Type u_1} {r : α → α → Prop} {a b : α} :
b = a b

theorem relation.refl_trans_gen_lift {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) :
(∀ (a b : α), r a bp (f a) (f b)) (f a) (f b)

theorem relation.refl_trans_gen_mono {α : Type u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} :
(∀ (a b : α), r a bp a b)

theorem relation.refl_trans_gen_eq_self {α : Type u_1} {r : α → α → Prop} :

theorem relation.reflexive_refl_trans_gen {α : Type u_1} {r : α → α → Prop} :

theorem relation.transitive_refl_trans_gen {α : Type u_1} {r : α → α → Prop} :

theorem relation.refl_trans_gen_idem {α : Type u_1} {r : α → α → Prop} :

theorem relation.refl_trans_gen_lift' {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {p : β → β → Prop} {a b : α} (f : α → β) :
(∀ (a b : α), r a b (f a) (f b)) (f a) (f b)

theorem relation.refl_trans_gen_closed {α : Type u_1} {r : α → α → Prop} {a b : α} {p : α → α → Prop} :
(∀ (a b : α), r a b b)

def relation.join {α : Type u_1} :
(α → α → Prop)α → α → Prop

The join of a relation on a single type is a new relation for which pairs of terms are related if there is a third term they are both related to. For example, if r is a relation representing rewrites in a term rewriting system, then confluence is the property that if a rewrites to both b and c, then join r relates b and c (see relation.church_rosser).

Equations
• = λ (a b : α), ∃ (c : α), r a c r b c
theorem relation.church_rosser {α : Type u_1} {r : α → α → Prop} {a b c : α} :
(∀ (a b c : α), r a br a c(∃ (d : α), d d))

theorem relation.join_of_single {α : Type u_1} {r : α → α → Prop} {a b : α} :
r a b b

theorem relation.symmetric_join {α : Type u_1} {r : α → α → Prop} :

theorem relation.reflexive_join {α : Type u_1} {r : α → α → Prop} :

theorem relation.transitive_join {α : Type u_1} {r : α → α → Prop} :
(∀ (a b c : α), r a br a c c)

theorem relation.equivalence_join {α : Type u_1} {r : α → α → Prop} :
(∀ (a b c : α), r a br a c c)

theorem relation.equivalence_join_refl_trans_gen {α : Type u_1} {r : α → α → Prop} :
(∀ (a b c : α), r a br a c(∃ (d : α), d d))

theorem relation.join_of_equivalence {α : Type u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} :
(∀ (a b : α), r' a br a b) a br a b

theorem relation.refl_trans_gen_of_transitive_reflexive {α : Type u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} :
(∀ (a b : α), r' a br a b) br a b

theorem relation.refl_trans_gen_of_equivalence {α : Type u_1} {r : α → α → Prop} {a b : α} {r' : α → α → Prop} :
(∀ (a b : α), r' a br a b) br a b

theorem relation.eqv_gen_iff_of_equivalence {α : Type u_1} {r : α → α → Prop} {a b : α} :
(eqv_gen r a b r a b)

theorem relation.eqv_gen_mono {α : Type u_1} {a b : α} {r p : α → α → Prop} :
(∀ (a b : α), r a bp a b) a b a b