data.list.chain

# 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.chain_iff {α : Type u_1} (R : α α Prop) (ᾰ : α) (ᾰ_1 : list α) :
ᾰ_1 ᾰ_1 = list.nil {b : α} {l : list α}, R ᾰ b b l ᾰ_1 = b :: l
theorem list.rel_of_chain_cons {α : Type u} {R : α α Prop} {a b : α} {l : list α} (p : a (b :: l)) :
R a b
theorem list.chain_of_chain_cons {α : Type u} {R : α α Prop} {a b : α} {l : list α} (p : a (b :: l)) :
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 : a l) :
b l
theorem list.chain.imp {α : Type u} {R S : α α Prop} (H : (a b : α), R a b S a b) {a : α} {l : list α} (p : a l) :
a l
theorem list.chain.iff {α : Type u} {R S : α α Prop} (H : (a b : α), R a b S a b) {a : α} {l : list α} :
a l a l
theorem list.chain.iff_mem {α : Type u} {R : α α Prop} {a : α} {l : list α} :
a l list.chain (λ (x y : α), x a :: l y l R x y) a l
theorem list.chain_singleton {α : Type u} {R : α α Prop} {a b : α} :
a [b] R a b
theorem list.chain_split {α : Type u} {R : α α Prop} {a b : α} {l₁ l₂ : list α} :
a (l₁ ++ b :: l₂) a (l₁ ++ [b]) b l₂
@[simp]
theorem list.chain_append_cons_cons {α : Type u} {R : α α Prop} {a b c : α} {l₁ l₂ : list α} :
a (l₁ ++ b :: c :: l₂) a (l₁ ++ [b]) R b c c l₂
theorem list.chain_iff_forall₂ {α : Type u} {R : α α Prop} {a : α} {l : list α} :
a l (a :: l.init) l
theorem list.chain_append_singleton_iff_forall₂ {α : Type u} {R : α α Prop} {l : list α} {a b : α} :
a (l ++ [b]) (a :: l) (l ++ [b])
theorem list.chain_map {α : Type u} {β : Type v} {R : α α Prop} (f : β α) {b : β} {l : list β} :
(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 : (f a) (list.map f l)) :
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 : a l) :
(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₁ : a l) (ha : p a) (hl₂ : (a : α), a l p a) :
(f a ha) 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₂ : (f a ha) l hl₁)) (H : (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) R a b) :
a l
@[protected]
theorem list.pairwise.chain {α : Type u} {R : α α Prop} {l : list α} {a : α} (p : (a :: l)) :
a l
@[protected]
theorem list.chain.pairwise {α : Type u} {R : α α Prop} [ R] {a : α} {l : list α} :
a l (a :: l)
theorem list.chain_iff_pairwise {α : Type u} {R : α α Prop} [ R] {a : α} {l : list α} :
a l (a :: l)
@[protected]
theorem list.chain.sublist {α : Type u} {R : α α Prop} {l₁ l₂ : list α} {a : α} [ R] (hl : a l₂) (h : l₁ <+ l₂) :
a l₁
@[protected]
theorem list.chain.rel {α : Type u} {R : α α Prop} {l : list α} {a b : α} [ R] (hl : a l) (hb : b l) :
R a b
theorem list.chain_iff_nth_le {α : Type u} {R : α α Prop} {a : α} {l : list α} :
a l ( (h : 0 < l.length), R a (l.nth_le 0 h)) (i : ) (h : i < l.length - 1), R (l.nth_le i _) (l.nth_le (i + 1) _)
theorem list.chain'.imp {α : Type u} {R S : α α Prop} (H : (a b : α), R a b S a b) {l : list α} (p : l) :
l
theorem list.chain'.iff {α : Type u} {R S : α α Prop} (H : (a b : α), R a b S a b) {l : list α} :
l l
theorem list.chain'.iff_mem {α : Type u} {R : α α Prop} {l : list α} :
l list.chain' (λ (x y : α), x l y l R x y) l
@[simp]
theorem list.chain'_nil {α : Type u} {R : α α Prop} :
@[simp]
theorem list.chain'_singleton {α : Type u} {R : α α Prop} (a : α) :
[a]
@[simp]
theorem list.chain'_cons {α : Type u} {R : α α Prop} {x y : α} {l : list α} :
(x :: y :: l) R x y (y :: l)
theorem list.chain'_is_infix {α : Type u} (l : list α) :
list.chain' (λ (x y : α), [x, y] <:+: l) l
theorem list.chain'_split {α : Type u} {R : α α Prop} {a : α} {l₁ l₂ : list α} :
(l₁ ++ a :: l₂) (l₁ ++ [a]) (a :: l₂)
@[simp]
theorem list.chain'_append_cons_cons {α : Type u} {R : α α Prop} {b c : α} {l₁ l₂ : list α} :
(l₁ ++ b :: c :: l₂) (l₁ ++ [b]) R b c (c :: l₂)
theorem list.chain'_map {α : Type u} {β : Type v} {R : α α Prop} (f : β α) {l : list β} :
(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.map f l)) :
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 : l) :
(list.map f l)
theorem list.pairwise.chain' {α : Type u} {R : α α Prop} {l : list α} :
l
theorem list.chain'_iff_pairwise {α : Type u} {R : α α Prop} [ R] {l : list α} :
l
@[protected]
theorem list.chain'.sublist {α : Type u} {R : α α Prop} {l₁ l₂ : list α} [ R] (hl : l₂) (h : l₁ <+ l₂) :
l₁
theorem list.chain'.cons {α : Type u} {R : α α Prop} {x y : α} {l : list α} (h₁ : R x y) (h₂ : (y :: l)) :
(x :: y :: l)
theorem list.chain'.tail {α : Type u} {R : α α Prop} {l : list α} (h : l) :
l.tail
theorem list.chain'.rel_head {α : Type u} {R : α α Prop} {x y : α} {l : list α} (h : (x :: y :: l)) :
R x y
theorem list.chain'.rel_head' {α : Type u} {R : α α Prop} {x : α} {l : list α} (h : (x :: l)) ⦃y : α⦄ (hy : y l.head') :
R x y
theorem list.chain'.cons' {α : Type u} {R : α α Prop} {x : α} {l : list α} :
l ( (y : α), y l.head' R x y) (x :: l)
theorem list.chain'_cons' {α : Type u} {R : α α Prop} {x : α} {l : list α} :
(x :: l) ( (y : α), y l.head' R x y) l
theorem list.chain'_append {α : Type u} {R : α α Prop} {l₁ l₂ : list α} :
(l₁ ++ l₂) l₁ l₂ (x : α), x l₁.last' (y : α), y l₂.head' R x y
theorem list.chain'.append {α : Type u} {R : α α Prop} {l₁ l₂ : list α} (h₁ : l₁) (h₂ : l₂) (h : (x : α), x l₁.last' (y : α), y l₂.head' R x y) :
(l₁ ++ l₂)
theorem list.chain'.left_of_append {α : Type u} {R : α α Prop} {l₁ l₂ : list α} (h : (l₁ ++ l₂)) :
l₁
theorem list.chain'.right_of_append {α : Type u} {R : α α Prop} {l₁ l₂ : list α} (h : (l₁ ++ l₂)) :
l₂
theorem list.chain'.infix {α : Type u} {R : α α Prop} {l l₁ : list α} (h : l) (h' : l₁ <:+: l) :
l₁
theorem list.chain'.suffix {α : Type u} {R : α α Prop} {l l₁ : list α} (h : l) (h' : l₁ <:+ l) :
l₁
theorem list.chain'.prefix {α : Type u} {R : α α Prop} {l l₁ : list α} (h : l) (h' : l₁ <+: l) :
l₁
theorem list.chain'.drop {α : Type u} {R : α α Prop} {l : list α} (h : l) (n : ) :
l)
theorem list.chain'.init {α : Type u} {R : α α Prop} {l : list α} (h : l) :
l.init
theorem list.chain'.take {α : Type u} {R : α α Prop} {l : list α} (h : l) (n : ) :
l)
theorem list.chain'_pair {α : Type u} {R : α α Prop} {x y : α} :
[x, y] R x y
theorem list.chain'.imp_head {α : Type u} {R : α α Prop} {x y : α} (h : {z : α}, R x z R y z) {l : list α} (hl : (x :: l)) :
(y :: l)
theorem list.chain'_reverse {α : Type u} {R : α α Prop} {l : list α} :
theorem list.chain'_iff_nth_le {α : Type u} {R : α α Prop} {l : list α} :
l (i : ) (h : i < l.length - 1), R (l.nth_le i _) (l.nth_le (i + 1) _)
theorem list.chain'.append_overlap {α : Type u} {R : α α Prop} {l₁ l₂ l₃ : list α} (h₁ : (l₁ ++ l₂)) (h₂ : (l₂ ++ l₃)) (hn : l₂ list.nil) :
(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 : b) :
(l : list α), a l (a :: l).last _ = 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 : 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 : 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₁ : a l) (hl₂ : (a :: l).last _ = 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.