mathlib docs: 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

relation.comp r p a c = ∃ (b : β), r a b ∧ p b c

source

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

relation.comp r eq = r

source

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

relation.comp eq r = r

source

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

relation.comp iff r = r

source

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

relation.comp r iff = r

source

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

relation.comp (relation.comp r p) q = relation.comp r (relation.comp p q)

source

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

flip (relation.comp r p) = relation.comp (flip p) (flip r)

source

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

relation.map r f g = λ (c : γ) (d : δ), ∃ (a : α) (b : β), r a b ∧ f a = c ∧ g b = d

source

inductive relation.refl_trans_gen {α : Type u_1} :

(α → α → Prop) → α → α → Prop

refl : ∀ {α : Type u_1} (r : α → α → Prop) (a : α), relation.refl_trans_gen r a a
tail : ∀ {α : Type u_1} (r : α → α → Prop) (a : α) {b c : α}, relation.refl_trans_gen r a b → r b c → relation.refl_trans_gen r a c

refl_trans_gen r: reflexive transitive closure of r

source

inductive relation.refl_gen {α : Type u_1} :

(α → α → Prop) → α → α → Prop

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

refl_gen r: reflexive closure of r

source

inductive relation.trans_gen {α : Type u_1} :

(α → α → Prop) → α → α → Prop

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

trans_gen r: transitive closure of r

source

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

relation.refl_gen r a b → relation.refl_trans_gen r a b

source

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

relation.refl_trans_gen r a b → relation.refl_trans_gen r b c → relation.refl_trans_gen r a c

source

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

r a b → relation.refl_trans_gen r a b

source

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

r a b → relation.refl_trans_gen r b c → relation.refl_trans_gen r a c

source

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

symmetric r → symmetric (relation.refl_trans_gen r)

source

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

relation.refl_trans_gen r a b → (b = a ∨ ∃ (c : α), relation.refl_trans_gen r a c ∧ r c b)

source

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

P b relation.refl_trans_gen.refl → (∀ {a c : α} (h' : r a c) (h : relation.refl_trans_gen r c b), P c h → P a _) → P a h

source

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

(∀ (a : α), P relation.refl_trans_gen.refl) → (∀ {a b : α} (h : r a b), P _) → (∀ {a b c : α} (h₁ : relation.refl_trans_gen r a b) (h₂ : relation.refl_trans_gen r b c), P h₁ → P h₂ → P _) → P h

source

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

relation.refl_trans_gen r a b → (a = b ∨ ∃ (c : α), r a c ∧ relation.refl_trans_gen r c b)

source

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

relation.refl_trans_gen r a b ↔ a = b ∨ ∃ (c : α), r a c ∧ relation.refl_trans_gen r c b

source

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

relator.right_unique r → relation.refl_trans_gen r a b → relation.refl_trans_gen r a c → relation.refl_trans_gen r b c ∨ relation.refl_trans_gen r c b

source

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

relation.trans_gen r a b → relation.refl_trans_gen r a b

source

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

relation.trans_gen r a b → relation.refl_trans_gen r b c → relation.trans_gen r a c

source

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

relation.trans_gen r a b → relation.trans_gen r b c → relation.trans_gen r a c

source

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

r a b → relation.refl_trans_gen r b c → relation.trans_gen r a c

source

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

relation.refl_trans_gen r a b → r b c → relation.trans_gen r a c

source

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

relation.refl_trans_gen r a b → relation.trans_gen r b c → relation.trans_gen r a c

source

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

r a b → relation.trans_gen r b c → relation.trans_gen r a c

source

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

relation.trans_gen r a c ↔ ∃ (b : α), relation.refl_trans_gen r a b ∧ r b c

source

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

relation.trans_gen r a c ↔ ∃ (b : α), r a b ∧ relation.refl_trans_gen r b c

source

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

(∀ (b : α), ¬r a b) → (relation.refl_trans_gen r a b ↔ b = a)

source

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

relation.refl_trans_gen r a b ↔ b = a ∨ relation.trans_gen r a b

source

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

(∀ (a b : α), r a b → p (f a) (f b)) → relation.refl_trans_gen r a b → relation.refl_trans_gen p (f a) (f b)

source

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

(∀ (a b : α), r a b → p a b) → relation.refl_trans_gen r a b → relation.refl_trans_gen p a b

source

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

reflexive r → transitive r → relation.refl_trans_gen r = r

source

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

reflexive (relation.refl_trans_gen r)

source

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

transitive (relation.refl_trans_gen r)

source

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

relation.refl_trans_gen (relation.refl_trans_gen r) = relation.refl_trans_gen r

source

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

(∀ (a b : α), r a b → relation.refl_trans_gen p (f a) (f b)) → relation.refl_trans_gen r a b → relation.refl_trans_gen p (f a) (f b)

source

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

(∀ (a b : α), r a b → relation.refl_trans_gen p a b) → relation.refl_trans_gen r a b → relation.refl_trans_gen p a b

source

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

relation.join r = λ (a b : α), ∃ (c : α), r a c ∧ r b c

source

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

(∀ (a b c : α), r a b → r a c → (∃ (d : α), relation.refl_gen r b d ∧ relation.refl_trans_gen r c d)) → relation.refl_trans_gen r a b → relation.refl_trans_gen r a c → relation.join (relation.refl_trans_gen r) b c

source

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

reflexive r → r a b → relation.join r a b

source

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

symmetric (relation.join r)

source

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

reflexive r → reflexive (relation.join r)

source

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

transitive r → (∀ (a b c : α), r a b → r a c → relation.join r b c) → transitive (relation.join r)

source

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

reflexive r → transitive r → (∀ (a b c : α), r a b → r a c → relation.join r b c) → equivalence (relation.join r)

source

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

(∀ (a b c : α), r a b → r a c → (∃ (d : α), relation.refl_gen r b d ∧ relation.refl_trans_gen r c d)) → equivalence (relation.join (relation.refl_trans_gen r))

source

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

equivalence r → (∀ (a b : α), r' a b → r a b) → relation.join r' a b → r a b

source

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

reflexive r → transitive r → (∀ (a b : α), r' a b → r a b) → relation.refl_trans_gen r' a b → r a b

source

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

equivalence r → (∀ (a b : α), r' a b → r a b) → relation.refl_trans_gen r' a b → r a b

source

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

equivalence r → (eqv_gen r a b ↔ r a b)

source

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

(∀ (a b : α), r a b → p a b) → eqv_gen r a b → eqv_gen p a b