mathlib documentation

data.list.chain

Relation chain #

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 α) :
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 α} (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)) :
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 α} (p : list.chain R a l) :
theorem list.chain.imp {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a bS a b) {a : α} {l : list α} (p : list.chain R 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₂
@[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_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)) :
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 α} (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 bS (f a ha) (f b hb)) {a : α} {l : list α} (hl₁ : list.chain R a l) (ha : p a) (hl₂ : ∀ (a : α), a lp 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 lp 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) :
theorem list.chain_of_pairwise {α : Type u} {R : α → α → Prop} {a : α} {l : list α} (p : list.pairwise 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 α} (p : list.chain' R l) :
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 : α) :
@[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)) :
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 α} (p : list.chain' R l) :
theorem list.pairwise.chain' {α : Type u} {R : α → α → Prop} {l : list α} :
theorem list.chain'_iff_pairwise {α : Type u} {R : α → α → Prop} (tr : transitive R) {l : list α} :
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) :
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'.drop {α : Type u} {R : α → α → Prop} (n : ) {l : list α} (h : 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'_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 α} (hl : 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 α} (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) :
∃ (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. 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 yp yp 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 yp yp 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) :

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.