def
relation.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3} :
(α → β → Prop) → (β → γ → Prop) → α → γ → Prop
Equations
- relation.comp r p a c = ∃ (b : β), r a b ∧ p b c
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)
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)
def
relation.map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4} :
(α → β → 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
- 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
- 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
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
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
theorem
relation.refl_trans_gen.single
{α : Type u_1}
{r : α → α → Prop}
{a b : α} :
r a b → relation.refl_trans_gen r a b
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
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)
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
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
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)
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
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
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
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
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
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
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
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
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
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
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
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)
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
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)
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
theorem
relation.refl_trans_gen_eq_self
{α : Type u_1}
{r : α → α → Prop} :
reflexive r → transitive r → relation.refl_trans_gen r = r
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)
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
Equations
- relation.join r = λ (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 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
theorem
relation.join_of_single
{α : Type u_1}
{r : α → α → Prop}
{a b : α} :
reflexive r → r a b → relation.join r a b
theorem
relation.reflexive_join
{α : Type u_1}
{r : α → α → Prop} :
reflexive r → reflexive (relation.join r)
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)
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)
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))
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
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
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
theorem
relation.eqv_gen_iff_of_equivalence
{α : Type u_1}
{r : α → α → Prop}
{a b : α} :
equivalence r → (eqv_gen r a b ↔ r a b)