mathlib documentation

data.list.chain

theorem list.chain_iff {α : Type u} (R : α → α → Prop) (ᾰ : α) (ᾰ_1 : list α) :
list.chain R ᾰ_1 ᾰ_1 = list.nil ∃ {b : α} {l : list α}, R ᾰ b list.chain R b l ᾰ_1 = b :: l

theorem list.rel_of_chain_cons {α : Type u} {R : α → α → Prop} {a b : α} {l : list α} :
list.chain R a (b :: l)R a b

theorem list.chain_of_chain_cons {α : Type u} {R : α → α → Prop} {a b : α} {l : list α} :
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 bS a b) {a b : α} (Hab : ∀ ⦃c : α⦄, R a cS b c) {l : list α} :
list.chain R a llist.chain S b l

theorem list.chain.imp {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a bS a b) {a : α} {l : list α} :
list.chain R a llist.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 α} :

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_singleton {α : Type u} {R : α → α → Prop} {a b : α} :
list.chain R a [b] R a b

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₂

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 α} :
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 bS (f a) (f b)) {a : α} {l : list α} :
list.chain R a llist.chain S (f a) (list.map f l)

theorem list.chain_of_pairwise {α : Type u} {R : α → α → Prop} {a : α} {l : list α} :
list.pairwise R (a :: l)list.chain R a l

theorem list.chain_iff_pairwise {α : Type u} {R : α → α → Prop} (tr : transitive R) {a : α} {l : list α} :

theorem list.chain_iff_nth_le {α : Type u} {R : α → α → Prop} {a : α} {l : list α} :
list.chain R 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 bS a b) {l : list α} :

theorem list.chain'.iff {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a b S a b) {l : list α} :

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]
theorem list.chain'_nil {α : Type u} {R : α → α → Prop} :

@[simp]
theorem list.chain'_singleton {α : Type u} {R : α → α → Prop} (a : α) :

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₂)

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 α} :

theorem list.chain'_map_of_chain' {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a bS (f a) (f b)) {l : list α} :

theorem list.pairwise.chain' {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.chain'_iff_pairwise {α : Type u} {R : α → α → Prop} (tr : transitive R) {l : list α} :

@[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'.cons {α : Type u} {R : α → α → Prop} {x y : α} {l : list α} :
R x ylist.chain' R (y :: l)list.chain' R (x :: y :: l)

theorem list.chain'.tail {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.chain'.rel_head {α : Type u} {R : α → α → Prop} {x y : α} {l : list α} :
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 : α⦄ :
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 α} :
list.chain' R l₁list.chain' R l₂(∀ (x : α), x l₁.last'∀ (y : α), y l₂.head'R x y)list.chain' R (l₁ ++ l₂)

theorem list.chain'_pair {α : Type u} {R : α → α → Prop} {x y : α} :
list.chain' R [x, y] R x y

theorem list.chain'.imp_head {α : Type u} {R : α → α → Prop} {x y : α} (h : ∀ {z : α}, R x zR y z) {l : list α} :
list.chain' R (x :: l)list.chain' R (y :: l)

theorem list.chain'_reverse {α : Type u} {R : α → α → Prop} {l : list α} :

theorem list.chain'_iff_nth_le {α : Type u} {R : α → α → Prop} {l : list α} :
list.chain' R 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 α} :
list.chain' R (l₁ ++ l₂)list.chain' R (l₂ ++ l₃)l₂ list.nillist.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 : α} :
relation.refl_trans_gen r a b(∃ (l : list α), list.chain r 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.

theorem list.chain.induction {α : Type u} {r : α → α → Prop} (p : α → Prop) {a b : α} (l : list α) :
list.chain r a l(a :: l).last _ = b(∀ {x y : α}, r x yp yp x)p bp 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 up the chain.