Relation chain #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides basic results about list.chain (definition in data.list.defs).
A list [a₂, ..., aₙ] is a chain starting at a₁ with respect to the relation r if r a₁ a₂
and r a₂ a₃ and ... and r aₙ₋₁ aₙ. We write it chain r a₁ [a₂, ..., aₙ].
A graph-specialized version is in development and will hopefully be added under combinatorics.
sometime soon.
theorem
list.rel_of_chain_cons
{α : Type u}
{R : α → α → Prop}
{a b : α}
{l : list α}
(p : list.chain R a (b :: l)) :
R a b
theorem
list.chain_of_chain_cons
{α : Type u}
{R : α → α → Prop}
{a b : α}
{l : list α}
(p : list.chain R a (b :: l)) :
list.chain R b l
theorem
list.chain.imp'
{α : Type u}
{R S : α → α → Prop}
(HRS : ∀ ⦃a b : α⦄, R a b → S a b)
{a b : α}
(Hab : ∀ ⦃c : α⦄, R a c → S b c)
{l : list α}
(p : list.chain R a l) :
list.chain S b l
theorem
list.chain.imp
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b)
{a : α}
{l : list α}
(p : list.chain R a l) :
list.chain S a l
theorem
list.chain.iff
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b ↔ S a b)
{a : α}
{l : list α} :
list.chain R a l ↔ list.chain S a l
theorem
list.chain.iff_mem
{α : Type u}
{R : α → α → Prop}
{a : α}
{l : list α} :
list.chain R a l ↔ list.chain (λ (x y : α), x ∈ a :: l ∧ y ∈ l ∧ R x y) a l
theorem
list.chain_split
{α : Type u}
{R : α → α → Prop}
{a b : α}
{l₁ l₂ : list α} :
list.chain R a (l₁ ++ b :: l₂) ↔ list.chain R a (l₁ ++ [b]) ∧ list.chain R b l₂
@[simp]
theorem
list.chain_append_cons_cons
{α : Type u}
{R : α → α → Prop}
{a b c : α}
{l₁ l₂ : list α} :
list.chain R a (l₁ ++ b :: c :: l₂) ↔ list.chain R a (l₁ ++ [b]) ∧ R b c ∧ list.chain R c l₂
theorem
list.chain_iff_forall₂
{α : Type u}
{R : α → α → Prop}
{a : α}
{l : list α} :
list.chain R a l ↔ l = list.nil ∨ list.forall₂ R (a :: l.init) l
theorem
list.chain_append_singleton_iff_forall₂
{α : Type u}
{R : α → α → Prop}
{l : list α}
{a b : α} :
list.chain R a (l ++ [b]) ↔ list.forall₂ R (a :: l) (l ++ [b])
theorem
list.chain_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
(f : β → α)
{b : β}
{l : list β} :
list.chain R (f b) (list.map f l) ↔ list.chain (λ (a b : β), R (f a) (f b)) b l
theorem
list.chain_of_chain_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), S (f a) (f b) → R a b)
{a : α}
{l : list α}
(p : list.chain S (f a) (list.map f l)) :
list.chain R a l
theorem
list.chain_map_of_chain
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), R a b → S (f a) (f b))
{a : α}
{l : list α}
(p : list.chain R a l) :
list.chain S (f a) (list.map f l)
theorem
list.chain_pmap_of_chain
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
{p : α → Prop}
{f : Π (a : α), p a → β}
(H : ∀ (a b : α) (ha : p a) (hb : p b), R a b → S (f a ha) (f b hb))
{a : α}
{l : list α}
(hl₁ : list.chain R a l)
(ha : p a)
(hl₂ : ∀ (a : α), a ∈ l → p a) :
list.chain S (f a ha) (list.pmap f l hl₂)
theorem
list.chain_of_chain_pmap
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
{p : α → Prop}
(f : Π (a : α), p a → β)
{l : list α}
(hl₁ : ∀ (a : α), a ∈ l → p a)
{a : α}
(ha : p a)
(hl₂ : list.chain S (f a ha) (list.pmap f l hl₁))
(H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b) :
list.chain R a l
@[protected]
theorem
list.pairwise.chain
{α : Type u}
{R : α → α → Prop}
{l : list α}
{a : α}
(p : list.pairwise R (a :: l)) :
list.chain R a l
@[protected]
theorem
list.chain.pairwise
{α : Type u}
{R : α → α → Prop}
[is_trans α R]
{a : α}
{l : list α} :
list.chain R a l → list.pairwise R (a :: l)
theorem
list.chain_iff_pairwise
{α : Type u}
{R : α → α → Prop}
[is_trans α R]
{a : α}
{l : list α} :
list.chain R a l ↔ list.pairwise R (a :: l)
@[protected]
theorem
list.chain.sublist
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ : list α}
{a : α}
[is_trans α R]
(hl : list.chain R a l₂)
(h : l₁ <+ l₂) :
list.chain R a l₁
@[protected]
theorem
list.chain.rel
{α : Type u}
{R : α → α → Prop}
{l : list α}
{a b : α}
[is_trans α R]
(hl : list.chain R a l)
(hb : b ∈ l) :
R a b
theorem
list.chain'.imp
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b → S a b)
{l : list α}
(p : list.chain' R l) :
list.chain' S l
theorem
list.chain'.iff
{α : Type u}
{R S : α → α → Prop}
(H : ∀ (a b : α), R a b ↔ S a b)
{l : list α} :
list.chain' R l ↔ list.chain' S l
theorem
list.chain'.iff_mem
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.chain' R l ↔ list.chain' (λ (x y : α), x ∈ l ∧ y ∈ l ∧ R x y) l
@[simp]
@[simp]
theorem
list.chain'_cons
{α : Type u}
{R : α → α → Prop}
{x y : α}
{l : list α} :
list.chain' R (x :: y :: l) ↔ R x y ∧ list.chain' R (y :: l)
theorem
list.chain'_split
{α : Type u}
{R : α → α → Prop}
{a : α}
{l₁ l₂ : list α} :
list.chain' R (l₁ ++ a :: l₂) ↔ list.chain' R (l₁ ++ [a]) ∧ list.chain' R (a :: l₂)
@[simp]
theorem
list.chain'_append_cons_cons
{α : Type u}
{R : α → α → Prop}
{b c : α}
{l₁ l₂ : list α} :
list.chain' R (l₁ ++ b :: c :: l₂) ↔ list.chain' R (l₁ ++ [b]) ∧ R b c ∧ list.chain' R (c :: l₂)
theorem
list.chain'_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
(f : β → α)
{l : list β} :
list.chain' R (list.map f l) ↔ list.chain' (λ (a b : β), R (f a) (f b)) l
theorem
list.chain'_of_chain'_map
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), S (f a) (f b) → R a b)
{l : list α}
(p : list.chain' S (list.map f l)) :
list.chain' R l
theorem
list.chain'_map_of_chain'
{α : Type u}
{β : Type v}
{R : α → α → Prop}
{S : β → β → Prop}
(f : α → β)
(H : ∀ (a b : α), R a b → S (f a) (f b))
{l : list α}
(p : list.chain' R l) :
list.chain' S (list.map f l)
theorem
list.pairwise.chain'
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.pairwise R l → list.chain' R l
theorem
list.chain'_iff_pairwise
{α : Type u}
{R : α → α → Prop}
[is_trans α R]
{l : list α} :
list.chain' R l ↔ list.pairwise R l
@[protected]
theorem
list.chain'.sublist
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ : list α}
[is_trans α R]
(hl : list.chain' R l₂)
(h : l₁ <+ l₂) :
list.chain' R l₁
theorem
list.chain'.cons
{α : Type u}
{R : α → α → Prop}
{x y : α}
{l : list α}
(h₁ : R x y)
(h₂ : list.chain' R (y :: l)) :
list.chain' R (x :: y :: l)
theorem
list.chain'.tail
{α : Type u}
{R : α → α → Prop}
{l : list α}
(h : list.chain' R l) :
list.chain' R l.tail
theorem
list.chain'.rel_head
{α : Type u}
{R : α → α → Prop}
{x y : α}
{l : list α}
(h : list.chain' R (x :: y :: l)) :
R x y
theorem
list.chain'.rel_head'
{α : Type u}
{R : α → α → Prop}
{x : α}
{l : list α}
(h : list.chain' R (x :: l))
⦃y : α⦄
(hy : y ∈ l.head') :
R x y
theorem
list.chain'.cons'
{α : Type u}
{R : α → α → Prop}
{x : α}
{l : list α} :
list.chain' R l → (∀ (y : α), y ∈ l.head' → R x y) → list.chain' R (x :: l)
theorem
list.chain'_cons'
{α : Type u}
{R : α → α → Prop}
{x : α}
{l : list α} :
list.chain' R (x :: l) ↔ (∀ (y : α), y ∈ l.head' → R x y) ∧ list.chain' R l
theorem
list.chain'.append
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ : list α}
(h₁ : list.chain' R l₁)
(h₂ : list.chain' R l₂)
(h : ∀ (x : α), x ∈ l₁.last' → ∀ (y : α), y ∈ l₂.head' → R x y) :
list.chain' R (l₁ ++ l₂)
theorem
list.chain'.left_of_append
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ : list α}
(h : list.chain' R (l₁ ++ l₂)) :
list.chain' R l₁
theorem
list.chain'.right_of_append
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ : list α}
(h : list.chain' R (l₁ ++ l₂)) :
list.chain' R l₂
theorem
list.chain'.infix
{α : Type u}
{R : α → α → Prop}
{l l₁ : list α}
(h : list.chain' R l)
(h' : l₁ <:+: l) :
list.chain' R l₁
theorem
list.chain'.suffix
{α : Type u}
{R : α → α → Prop}
{l l₁ : list α}
(h : list.chain' R l)
(h' : l₁ <:+ l) :
list.chain' R l₁
theorem
list.chain'.prefix
{α : Type u}
{R : α → α → Prop}
{l l₁ : list α}
(h : list.chain' R l)
(h' : l₁ <+: l) :
list.chain' R l₁
theorem
list.chain'.drop
{α : Type u}
{R : α → α → Prop}
{l : list α}
(h : list.chain' R l)
(n : ℕ) :
list.chain' R (list.drop n l)
theorem
list.chain'.init
{α : Type u}
{R : α → α → Prop}
{l : list α}
(h : list.chain' R l) :
list.chain' R l.init
theorem
list.chain'.take
{α : Type u}
{R : α → α → Prop}
{l : list α}
(h : list.chain' R l)
(n : ℕ) :
list.chain' R (list.take n l)
theorem
list.chain'.imp_head
{α : Type u}
{R : α → α → Prop}
{x y : α}
(h : ∀ {z : α}, R x z → R y z)
{l : list α}
(hl : list.chain' R (x :: l)) :
list.chain' R (y :: l)
theorem
list.chain'_reverse
{α : Type u}
{R : α → α → Prop}
{l : list α} :
list.chain' R l.reverse ↔ list.chain' (flip R) l
theorem
list.chain'.append_overlap
{α : Type u}
{R : α → α → Prop}
{l₁ l₂ l₃ : list α}
(h₁ : list.chain' R (l₁ ++ l₂))
(h₂ : list.chain' R (l₂ ++ l₃))
(hn : l₂ ≠ list.nil) :
list.chain' R (l₁ ++ l₂ ++ l₃)
If l₁ l₂ and l₃ are lists and l₁ ++ l₂ and l₂ ++ l₃ both satisfy
chain' R, then so does l₁ ++ l₂ ++ l₃ provided l₂ ≠ []
theorem
list.exists_chain_of_relation_refl_trans_gen
{α : Type u}
{r : α → α → Prop}
{a b : α}
(h : relation.refl_trans_gen r a b) :
If a and b are related by the reflexive transitive closure of r, then there is a r-chain
starting from a and ending on b.
The converse of relation_refl_trans_gen_of_exists_chain.
theorem
list.chain.induction
{α : Type u}
{r : α → α → Prop}
{a b : α}
(p : α → Prop)
(l : list α)
(h : list.chain r a l)
(hb : (a :: l).last _ = b)
(carries : ∀ ⦃x y : α⦄, r x y → p y → p x)
(final : p b)
(i : α)
(H : i ∈ a :: l) :
p i
Given a chain from a to b, and a predicate true at b, if r x y → p y → p x then
the predicate is true everywhere in the chain and at a.
That is, we can propagate the predicate up the chain.
theorem
list.chain.induction_head
{α : Type u}
{r : α → α → Prop}
{a b : α}
(p : α → Prop)
(l : list α)
(h : list.chain r a l)
(hb : (a :: l).last _ = b)
(carries : ∀ ⦃x y : α⦄, r x y → p y → p x)
(final : p b) :
p a
Given a chain from a to b, and a predicate true at b, if r x y → p y → p x then
the predicate is true at a.
That is, we can propagate the predicate all the way up the chain.
theorem
list.relation_refl_trans_gen_of_exists_chain
{α : Type u}
{r : α → α → Prop}
{a b : α}
(l : list α)
(hl₁ : list.chain r a l)
(hl₂ : (a :: l).last _ = b) :
relation.refl_trans_gen r a b
If there is an r-chain starting from a and ending at b, then a and b are related by the
reflexive transitive closure of r. The converse of exists_chain_of_relation_refl_trans_gen.