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) (a✝ : α) (a✝¹ : List α) : Chain R a✝ a✝¹ ↔ a✝¹ = [] ∨ ∃ (b : α), ∃ (l : List α), R a✝ b ∧ Chain R b l ∧ a✝¹ = b :: l

theorem List.Chain.iff {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a b ↔ S a b) {a : α} {l : List α} : Chain R a l ↔ Chain S a l

theorem List.Chain.iff_mem {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : Chain R a l ↔ Chain (fun (x y : α) => x ∈ a :: l ∧ y ∈ l ∧ R x y) a l

theorem List.chain_singleton {α : Type u} {R : α → α → Prop} {a b : α} : Chain R a [b] ↔ R a b

theorem List.chain_split {α : Type u} {R : α → α → Prop} {a b : α} {l₁ l₂ : List α} : Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂

@[simp]

theorem List.chain_append_cons_cons {α : Type u} {R : α → α → Prop} {a b c : α} {l₁ l₂ : List α} : Chain R a (l₁ ++ b :: c :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ R b c ∧ Chain R c l₂

theorem List.chain_iff_forall₂ {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : Chain R a l ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l

theorem List.chain_append_singleton_iff_forall₂ {α : Type u} {R : α → α → Prop} {l : List α} {a b : α} : Chain R a (l ++ [b]) ↔ Forall₂ R (a :: l) (l ++ [b])

theorem List.chain_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {b : β} {l : List β} : Chain R (f b) (map f l) ↔ Chain (fun (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 : Chain S (f a) (map f l)) : 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 : Chain R a l) : Chain S (f a) (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₁ : Chain R a l) (ha : p a) (hl₂ : ∀ (a : α), a ∈ l → p a) : Chain S (f a ha) (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₂ : Chain S (f a ha) (pmap f l hl₁)) (H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b) : Chain R a l

theorem List.Chain.pairwise {α : Type u} {R : α → α → Prop} [IsTrans α R] {a : α} {l : List α} : Chain R a l → Pairwise R (a :: l)

theorem List.chain_iff_pairwise {α : Type u} {R : α → α → Prop} [IsTrans α R] {a : α} {l : List α} : Chain R a l ↔ Pairwise R (a :: l)

theorem List.Chain.sublist {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} {a : α} [IsTrans α R] (hl : Chain R a l₂) (h : l₁.Sublist l₂) : Chain R a l₁

theorem List.Chain.rel {α : Type u} {R : α → α → Prop} {l : List α} {a b : α} [IsTrans α R] (hl : Chain R a l) (hb : b ∈ l) : R a b

theorem List.chain_iff_get {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : Chain R a l ↔ (∀ (h : 0 < l.length), R a (l.get ⟨0, h⟩)) ∧ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)

theorem List.chain_replicate_of_rel {α : Type u} {r : α → α → Prop} (n : ℕ) {a : α} (h : r a a) : Chain r a (replicate n a)

theorem List.chain_eq_iff_eq_replicate {α : Type u} {a : α} {l : List α} : Chain (fun (x1 x2 : α) => x1 = x2) a l ↔ l = replicate l.length a

theorem List.Chain'.imp {α : Type u} {R S : α → α → Prop} (H : ∀ (a b : α), R a b → S a b) {l : List α} (p : Chain' R l) : Chain' S l

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

theorem List.Chain'.iff_mem {α : Type u} {R : α → α → Prop} {l : List α} : Chain' R l ↔ Chain' (fun (x y : α) => x ∈ l ∧ y ∈ l ∧ R x y) l

@[simp]

theorem List.chain'_nil {α : Type u} {R : α → α → Prop} : Chain' R []

@[simp]

theorem List.chain'_singleton {α : Type u} {R : α → α → Prop} (a : α) : Chain' R [a]

@[simp]

theorem List.chain'_cons_cons {α : Type u} {R : α → α → Prop} {x y : α} {l : List α} : Chain' R (x :: y :: l) ↔ R x y ∧ Chain' R (y :: l)

@[deprecated List.chain'_cons_cons (since := "2025-08-12")]

theorem List.chain'_cons {α : Type u} {R : α → α → Prop} {x y : α} {l : List α} : Chain' R (x :: y :: l) ↔ R x y ∧ Chain' R (y :: l)

Alias of List.chain'_cons_cons.

theorem List.chain'_isInfix {α : Type u} (l : List α) : Chain' (fun (x y : α) => [x, y] <:+: l) l

theorem List.chain'_split {α : Type u} {R : α → α → Prop} {a : α} {l₁ l₂ : List α} : Chain' R (l₁ ++ a :: l₂) ↔ Chain' R (l₁ ++ [a]) ∧ Chain' R (a :: l₂)

@[simp]

theorem List.chain'_append_cons_cons {α : Type u} {R : α → α → Prop} {b c : α} {l₁ l₂ : List α} : Chain' R (l₁ ++ b :: c :: l₂) ↔ Chain' R (l₁ ++ [b]) ∧ R b c ∧ Chain' R (c :: l₂)

theorem List.chain'_iff_forall_rel_of_append_cons_cons {α : Type u} {R : α → α → Prop} {l : List α} : Chain' R l ↔ ∀ ⦃a b : α⦄ ⦃l₁ l₂ : List α⦄, l = l₁ ++ a :: b :: l₂ → R a b

theorem List.chain'_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : List β} : Chain' R (map f l) ↔ Chain' (fun (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 : Chain' S (map f l)) : 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 : Chain' R l) : Chain' S (map f l)

theorem List.Pairwise.chain' {α : Type u} {R : α → α → Prop} {l : List α} : Pairwise R l → Chain' R l

theorem List.chain'_iff_pairwise {α : Type u} {R : α → α → Prop} [IsTrans α R] {l : List α} : Chain' R l ↔ Pairwise R l

theorem List.Chain'.sublist {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} [IsTrans α R] (hl : Chain' R l₂) (h : l₁.Sublist l₂) : Chain' R l₁

theorem List.Chain'.cons_cons {α : Type u} {R : α → α → Prop} {x y : α} {l : List α} (h₁ : R x y) (h₂ : Chain' R (y :: l)) : Chain' R (x :: y :: l)

@[deprecated List.Chain'.cons_cons (since := "2025-08-12")]

theorem List.Chain'.cons {α : Type u} {R : α → α → Prop} {x y : α} {l : List α} (h₁ : R x y) (h₂ : Chain' R (y :: l)) : Chain' R (x :: y :: l)

Alias of List.Chain'.cons_cons.

theorem List.Chain'.tail {α : Type u} {R : α → α → Prop} {l : List α} : Chain' R l → Chain' R l.tail

theorem List.Chain'.rel_head {α : Type u} {R : α → α → Prop} {x y : α} {l : List α} (h : Chain' R (x :: y :: l)) : R x y

theorem List.Chain'.rel_head? {α : Type u} {R : α → α → Prop} {x : α} {l : List α} (h : Chain' R (x :: l)) ⦃y : α⦄ (hy : y ∈ l.head?) : R x y

theorem List.Chain'.cons' {α : Type u} {R : α → α → Prop} {x : α} {l : List α} : Chain' R l → (∀ (y : α), y ∈ l.head? → R x y) → Chain' R (x :: l)

theorem List.Chain'.cons_of_ne_nil {α : Type u} {R : α → α → Prop} {x : α} {l : List α} (l_ne_nil : l ≠ []) (hl : Chain' R l) (h : R x (l.head l_ne_nil)) : Chain' R (x :: l)

theorem List.chain'_cons' {α : Type u} {R : α → α → Prop} {x : α} {l : List α} : Chain' R (x :: l) ↔ (∀ (y : α), y ∈ l.head? → R x y) ∧ Chain' R l

theorem List.chain'_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} : Chain' R (l₁ ++ l₂) ↔ Chain' R l₁ ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

theorem List.Chain'.append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} (h₁ : Chain' R l₁) (h₂ : Chain' R l₂) (h : ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) : Chain' R (l₁ ++ l₂)

theorem List.Chain'.left_of_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} (h : Chain' R (l₁ ++ l₂)) : Chain' R l₁

theorem List.Chain'.right_of_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} (h : Chain' R (l₁ ++ l₂)) : Chain' R l₂

theorem List.Chain'.infix {α : Type u} {R : α → α → Prop} {l l₁ : List α} (h : Chain' R l) (h' : l₁ <:+: l) : Chain' R l₁

theorem List.Chain'.suffix {α : Type u} {R : α → α → Prop} {l l₁ : List α} (h : Chain' R l) (h' : l₁ <:+ l) : Chain' R l₁

theorem List.Chain'.prefix {α : Type u} {R : α → α → Prop} {l l₁ : List α} (h : Chain' R l) (h' : l₁ <+: l) : Chain' R l₁

theorem List.Chain'.drop {α : Type u} {R : α → α → Prop} {l : List α} (h : Chain' R l) (n : ℕ) : Chain' R (List.drop n l)

theorem List.Chain'.init {α : Type u} {R : α → α → Prop} {l : List α} (h : Chain' R l) : Chain' R l.dropLast

theorem List.Chain'.take {α : Type u} {R : α → α → Prop} {l : List α} (h : Chain' R l) (n : ℕ) : Chain' R (List.take n l)

theorem List.chain'_pair {α : Type u} {R : α → α → Prop} {x y : α} : Chain' R [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 : Chain' R (x :: l)) : Chain' R (y :: l)

theorem List.Chain'.getElem {α : Type u} {R : α → α → Prop} {l : List α} (h : Chain' R l) (n : ℕ) (h' : n + 1 < l.length) : R l[n] l[n + 1]

theorem List.chain'_of_not {α : Type u} {R : α → α → Prop} {l : List α} (h : ¬Chain' R l) : ∃ (n : ℕ), ∃ (h : n + 1 < l.length), ¬R l[n] l[n + 1]

theorem List.chain'_iff_forall_getElem {α : Type u} {R : α → α → Prop} {l : List α} : Chain' R l ↔ ∀ (n : ℕ) (h : n + 1 < l.length), R l[n] l[n + 1]

theorem List.chain'_reverse {α : Type u} {R : α → α → Prop} {l : List α} : Chain' R l.reverse ↔ Chain' (flip R) l

theorem List.chain'_iff_get {α : Type u} {R : α → α → Prop} {l : List α} : Chain' R l ↔ ∀ (i : ℕ) (h : i < l.length - 1), R (l.get ⟨i, ⋯⟩) (l.get ⟨i + 1, ⋯⟩)

theorem List.Chain'.append_overlap {α : Type u} {R : α → α → Prop} {l₁ l₂ l₃ : List α} (h₁ : Chain' R (l₁ ++ l₂)) (h₂ : Chain' R (l₂ ++ l₃)) (hn : l₂ ≠ []) : 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.chain'_flatten {α : Type u} {R : α → α → Prop} {L : List (List α)} : ¬[] ∈ L → (Chain' R L.flatten ↔ (∀ (l : List α), l ∈ L → Chain' R l) ∧ Chain' (fun (l₁ l₂ : List α) => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) L)

theorem List.chain'_attachWith {α : Type u} {l : List α} {p : α → Prop} (h : ∀ (x : α), x ∈ l → p x) {r : { a : α // p a } → { a : α // p a } → Prop} : Chain' r (l.attachWith p h) ↔ Chain' (fun (a b : α) => ∃ (ha : p a), ∃ (hb : p b), r ⟨a, ha⟩ ⟨b, hb⟩) l

theorem List.chain'_attach {α : Type u} {l : List α} {r : { a : α // a ∈ l } → { a : α // a ∈ l } → Prop} : Chain' r l.attach ↔ Chain' (fun (a b : α) => ∃ (ha : a ∈ l), ∃ (hb : b ∈ l), r ⟨a, ha⟩ ⟨b, hb⟩) l

theorem List.exists_chain_of_relationReflTransGen {α : Type u} {r : α → α → Prop} {a b : α} (h : Relation.ReflTransGen r a b) : ∃ (l : List α), Chain r a l ∧ (a :: l).getLast ⋯ = b

If a and b are related by the reflexive transitive closure of r, then there is an r-chain starting from a and ending on b. The converse of relationReflTransGen_of_exists_chain.

theorem List.Chain.induction {α : Type u} {r : α → α → Prop} {a : α} (p : α → Prop) (l : List α) (h : Chain r a l) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) (i : α) : i ∈ l → p i

Given a chain from a to b, and a predicate true at a, if r x y → p x → p y then the predicate is true everywhere in the chain. That is, we can propagate the predicate down the chain.

theorem List.Chain'.induction {α : Type u} {r : α → α → Prop} (p : α → Prop) (l : List α) (h : Chain' r l) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : ∀ (lne : l ≠ []), p (l.head lne)) (i : α) : i ∈ l → p i

A version of List.Chain.induction for List.Chain'

theorem List.Chain.backwards_induction {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : Chain r a l) (hb : (a :: l).getLast ⋯ = b) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) (i : α) : 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.backwards_induction_head {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : Chain r a l) (hb : (a :: l).getLast ⋯ = 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.relationReflTransGen_of_exists_chain {α : Type u} {r : α → α → Prop} {a b : α} (l : List α) (hl₁ : Chain r a l) (hl₂ : (a :: l).getLast ⋯ = b) : Relation.ReflTransGen 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_relationReflTransGen.

theorem List.Chain'.cons_of_le {α : Type u} [LinearOrder α] {a : α} {as m : List α} (ha : Chain' (fun (x1 x2 : α) => x1 > x2) (a :: as)) (hm : Chain' (fun (x1 x2 : α) => x1 > x2) m) (hmas : m ≤ as) : Chain' (fun (x1 x2 : α) => x1 > x2) (a :: m)

theorem List.Chain'.chain {α : Type u_1} {R : α → α → Prop} {l : List α} {v : α} (hl : Chain' R l) (hv : ∀ (lne : l ≠ []), R v (l.head lne)) : Chain R v l

theorem List.Chain'.iterate_eq_of_apply_eq {α : Type u_1} {f : α → α} {l : List α} (hl : Chain' (fun (x y : α) => f x = y) l) (i : ℕ) (hi : i < l.length) : f^[i] l[0] = l[i]

theorem List.chain'_replicate_of_rel {α : Type u} {r : α → α → Prop} (n : ℕ) {a : α} (h : r a a) : Chain' r (replicate n a)

theorem List.chain'_eq_iff_eq_replicate {α : Type u} {l : List α} : Chain' (fun (x1 x2 : α) => x1 = x2) l ↔ ∀ (a : α), a ∈ l.head? → l = replicate l.length a

In this section, we consider the type of r-decreasing chains (List.Chain' (flip r)) equipped with lexicographic order List.Lex r.

@[reducible, inline]

abbrev List.chains {α : Type u_1} (r : α → α → Prop) : Type u_1

The type of r-decreasing chains

Equations

• List.chains r = { l : List α // List.Chain' (flip r) l }

@[reducible, inline]

abbrev List.lex_chains {α : Type u_1} (r : α → α → Prop) (l m : chains r) : Prop

The lexicographic order on the r-decreasing chains

Equations

• List.lex_chains r l m = List.Lex r ↑l ↑m

theorem Acc.list_chain' {α : Type u_1} {r : α → α → Prop} {l : List.chains r} (acc : ∀ (a : α), a ∈ (↑l).head? → Acc r a) : Acc (List.lex_chains r) l

If an r-decreasing chain l is empty or its head is accessible by r, then l is accessible by the lexicographic order List.Lex r.

theorem WellFounded.list_chain' {α : Type u_1} {r : α → α → Prop} (hwf : WellFounded r) : WellFounded (List.lex_chains r)

If r is well-founded, the lexicographic order on r-decreasing chains is also.

instance instIsWellFoundedChainsLex_chains {α : Type u_1} {r : α → α → Prop} [hwf : IsWellFounded α r] : IsWellFounded (List.chains r) (List.lex_chains r)