Relation chain

This file provides basic results about List.IsChain from betteries. A list [a₁, a₂, ..., aₙ] satifies IsChain with respect to the relation r if r a₁ a₂ and r a₂ a₃ and ... and r aₙ₋₁ aₙ. We write it IsChain r [a₁, a₂, ..., aₙ]. A graph-specialized version is in development and will hopefully be added under combinatorics. sometime soon.

theorem List.isChain_iff {α : Type u_1} (R : α → α → Prop) (a✝ : List α) : IsChain R a✝ ↔ a✝ = [] ∨ (∃ (a : α), a✝ = [a]) ∨ ∃ (a : α), ∃ (b : α), ∃ (l : List α), R a b ∧ IsChain R (b :: l) ∧ a✝ = a :: b :: l

theorem List.isChain_nil {α : Type u} {R : α → α → Prop} : IsChain R []

theorem List.isChain_singleton {α : Type u} {R : α → α → Prop} (a : α) : IsChain R [a]

@[deprecated List.isChain_nil (since := "2025-09-24")]

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

Alias of List.isChain_nil.

@[deprecated List.isChain_singleton (since := "2025-09-24")]

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

Alias of List.isChain_singleton.

@[deprecated List.isChain_cons_cons (since := "2025-09-24")]

theorem List.chain'_cons_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)

Alias of List.isChain_cons_cons.

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

theorem List.chain'_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)

Alias of List.isChain_cons_cons.

@[deprecated List.IsChain.cons_cons (since := "2025-09-24")]

def List.Chain'.cons_cons {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α} (hr : R a b) (h : IsChain R (b :: l)) : IsChain R (a :: b :: l)

Alias of List.IsChain.cons_cons.

---

If a relates to b and b::l is a chain, then a :: b :: l is also a chain.

Equations

• @List.Chain'.cons_cons = @List.IsChain.cons_cons

@[deprecated List.IsChain.cons_cons (since := "2025-09-24")]

def List.Chain'.cons {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α} (hr : R a b) (h : IsChain R (b :: l)) : IsChain R (a :: b :: l)

Alias of List.IsChain.cons_cons.

---

If a relates to b and b::l is a chain, then a :: b :: l is also a chain.

Equations

• @List.Chain'.cons = @List.IsChain.cons_cons

theorem List.isChain_cons_iff {α : Type u} (R : α → α → Prop) (a : α) (l : List α) : IsChain R (a :: l) ↔ l = [] ∨ ∃ (b : α), ∃ (l' : List α), R a b ∧ IsChain R (b :: l') ∧ l = b :: l'

@[deprecated List.isChain_cons_iff (since := "2025-09-24")]

theorem List.chain_iff {α : Type u} (R : α → α → Prop) (a : α) (l : List α) : IsChain R (a :: l) ↔ l = [] ∨ ∃ (b : α), ∃ (l' : List α), R a b ∧ IsChain R (b :: l') ∧ l = b :: l'

Alias of List.isChain_cons_iff.

theorem List.IsChain.imp_of_mem_tail_imp {α : Type u} {R S : α → α → Prop} {l : List α} (H : ∀ (a b : α), a ∈ l → b ∈ l.tail → R a b → S a b) (p : IsChain R l) : IsChain S l

theorem List.IsChain.imp_of_mem_imp {α : Type u} {R S : α → α → Prop} {l : List α} (H : ∀ (a b : α), a ∈ l → b ∈ l → R a b → S a b) (p : IsChain R l) : IsChain S l

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

@[deprecated List.IsChain.iff (since := "2025-09-24")]

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

Alias of List.IsChain.iff.

@[deprecated List.IsChain.imp (since := "2025-09-24")]

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

Alias of List.IsChain.imp.

@[deprecated List.IsChain.iff (since := "2025-09-24")]

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

Alias of List.IsChain.iff.

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

theorem List.IsChain.iff_of_mem_tail_imp {α : Type u} {R S : α → α → Prop} {l : List α} (H : ∀ (a b : α), a ∈ l → b ∈ l.tail → (R a b ↔ S a b)) : IsChain R l ↔ IsChain S l

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

theorem List.IsChain.iff_mem_mem_tail {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l ↔ IsChain (fun (x y : α) => x ∈ l ∧ y ∈ l.tail ∧ R x y) l

@[deprecated List.IsChain.iff_mem (since := "2025-09-24")]

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

Alias of List.IsChain.iff_mem.

@[deprecated List.IsChain.iff_mem_mem_tail (since := "2025-09-24")]

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

Alias of List.IsChain.iff_mem_mem_tail.

@[deprecated List.isChain_cons_cons (since := "2025-09-24")]

theorem List.isChain_cons {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {a b : α✝} {l : List α✝} : IsChain R (a :: b :: l) ↔ R a b ∧ IsChain R (b :: l)

Alias of List.isChain_cons_cons.

theorem List.isChain_pair {α : Type u} {R : α → α → Prop} {x y : α} : IsChain R [x, y] ↔ R x y

@[deprecated List.isChain_pair (since := "2025-09-24")]

theorem List.chain_singleton {α : Type u} {R : α → α → Prop} {x y : α} : IsChain R [x, y] ↔ R x y

Alias of List.isChain_pair.

@[deprecated List.isChain_pair (since := "2025-09-24")]

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

Alias of List.isChain_pair.

theorem List.isChain_isInfix {α : Type u} (l : List α) : IsChain (fun (x y : α) => [x, y] <:+: l) l

@[deprecated List.isChain_isInfix (since := "2025-09-24")]

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

Alias of List.isChain_isInfix.

theorem List.isChain_split {α : Type u} {R : α → α → Prop} {c : α} {l₁ l₂ : List α} : IsChain R (l₁ ++ c :: l₂) ↔ IsChain R (l₁ ++ [c]) ∧ IsChain R (c :: l₂)

@[deprecated List.isChain_split (since := "2025-09-24")]

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

Alias of List.isChain_split.

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

@[deprecated List.isChain_cons_split (since := "2025-09-19")]

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

Alias of List.isChain_cons_split.

@[simp]

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

@[deprecated List.isChain_append_cons_cons (since := "2025-09-24")]

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

Alias of List.isChain_append_cons_cons.

@[simp]

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

@[deprecated List.isChain_cons_append_cons_cons (since := "2025-09-19")]

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

Alias of List.isChain_cons_append_cons_cons.

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

@[deprecated List.isChain_append_cons_cons (since := "2025-09-24")]

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

Alias of List.isChain_append_cons_cons.

theorem List.isChain_iff_forall₂ {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l ↔ Forall₂ R l.dropLast l.tail

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

@[deprecated List.isChain_cons_iff_forall₂ (since := "2025-09-24")]

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

Alias of List.isChain_cons_iff_forall₂.

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

@[deprecated List.isChain_cons_append_singleton_iff_forall₂ (since := "2025-09-24")]

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

Alias of List.isChain_cons_append_singleton_iff_forall₂.

theorem List.isChain_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : List β} : IsChain R (map f l) ↔ IsChain (fun (a b : β) => R (f a) (f b)) l

@[deprecated List.isChain_map (since := "2025-09-24")]

theorem List.chain'_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : List β} : IsChain R (map f l) ↔ IsChain (fun (a b : β) => R (f a) (f b)) l

Alias of List.isChain_map.

theorem List.isChain_of_isChain_map {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), S (f a) (f b) → R a b) {l : List α} (p : IsChain S (map f l)) : IsChain R l

@[deprecated List.isChain_of_isChain_map (since := "2025-09-24")]

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 : IsChain S (map f l)) : IsChain R l

Alias of List.isChain_of_isChain_map.

theorem List.isChain_map_of_isChain {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) {l : List α} (p : IsChain R l) : IsChain S (map f l)

@[deprecated List.isChain_map_of_isChain (since := "2025-09-24")]

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 : IsChain R l) : IsChain S (map f l)

Alias of List.isChain_map_of_isChain.

theorem List.isChain_cons_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : List β} {b : β} : IsChain R (f b :: map f l) ↔ IsChain (fun (a b : β) => R (f a) (f b)) (b :: l)

theorem List.isChain_cons_of_isChain_cons_map {α : Type u} {β : Type v} {R : α → α → Prop} {a : α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), S (f a) (f b) → R a b) {l : List α} (p : IsChain S (f a :: map f l)) : IsChain R (a :: l)

theorem List.isChain_cons_map_of_isChain_cons {α : Type u} {β : Type v} {R : α → α → Prop} {a : α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) {l : List α} (p : IsChain R (a :: l)) : IsChain S (f a :: map f l)

@[deprecated List.isChain_cons_map (since := "2025-09-19")]

theorem List.chain_map {α : Type u} {β : Type v} {R : α → α → Prop} (f : β → α) {l : List β} {b : β} : IsChain R (f b :: map f l) ↔ IsChain (fun (a b : β) => R (f a) (f b)) (b :: l)

Alias of List.isChain_cons_map.

@[deprecated List.isChain_cons_of_isChain_cons_map (since := "2025-09-19")]

theorem List.chain_of_chain_map {α : Type u} {β : Type v} {R : α → α → Prop} {a : α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), S (f a) (f b) → R a b) {l : List α} (p : IsChain S (f a :: map f l)) : IsChain R (a :: l)

Alias of List.isChain_cons_of_isChain_cons_map.

@[deprecated List.isChain_cons_map_of_isChain_cons (since := "2025-09-19")]

theorem List.chain_map_of_chain {α : Type u} {β : Type v} {R : α → α → Prop} {a : α} {S : β → β → Prop} (f : α → β) (H : ∀ (a b : α), R a b → S (f a) (f b)) {l : List α} (p : IsChain R (a :: l)) : IsChain S (f a :: map f l)

Alias of List.isChain_cons_map_of_isChain_cons.

theorem List.isChain_pmap {α : Type u} {β : Type v} {S : β → β → Prop} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (hl : ∀ (a : α), a ∈ l → p a) : IsChain S (pmap f l hl) ↔ IsChain (fun (a b : α) => ∃ (ha : p a), ∃ (hb : p b), S (f a ha) (f b hb)) l

theorem List.isChain_pmap_of_isChain {α : 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)) {l : List α} (hl₁ : IsChain R l) (hl₂ : ∀ (a : α), a ∈ l → p a) : IsChain S (pmap f l hl₂)

theorem List.isChain_of_isChain_pmap {α : Type u} {β : Type v} {R : α → α → Prop} {S : β → β → Prop} {p : α → Prop} (f : (a : α) → p a → β) {l : List α} (hl₁ : ∀ (a : α), a ∈ l → p a) (hl₂ : IsChain S (pmap f l hl₁)) (H : ∀ (a b : α) (ha : p a) (hb : p b), S (f a ha) (f b hb) → R a b) : IsChain R l

theorem List.isChain_cons_pmap {α : Type u} {β : Type v} {R : α → α → Prop} {p : β → Prop} (f : (b : β) → p b → α) {l : List β} (hl : ∀ (b : β), b ∈ l → p b) {a : β} (ha : p a) : IsChain R (f a ha :: pmap f l hl) ↔ IsChain (fun (a b : β) => ∃ (ha : p a), ∃ (hb : p b), R (f a ha) (f b hb)) (a :: l)

theorem List.isChain_cons_pmap_of_isChain_cons {α : 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)) {l : List α} {a : α} (ha : p a) (hl₁ : IsChain R (a :: l)) (hl₂ : ∀ (a : α), a ∈ l → p a) : IsChain S (f a ha :: pmap f l hl₂)

theorem List.isChain_cons_of_isChain_cons_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₂ : IsChain 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) : IsChain R (a :: l)

@[deprecated List.isChain_cons_pmap_of_isChain_cons (since := "2025-09-19")]

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)) {l : List α} {a : α} (ha : p a) (hl₁ : IsChain R (a :: l)) (hl₂ : ∀ (a : α), a ∈ l → p a) : IsChain S (f a ha :: pmap f l hl₂)

Alias of List.isChain_cons_pmap_of_isChain_cons.

@[deprecated List.isChain_cons_of_isChain_cons_pmap (since := "2025-09-19")]

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₂ : IsChain 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) : IsChain R (a :: l)

Alias of List.isChain_cons_of_isChain_cons_pmap.

@[deprecated List.IsChain.pairwise (since := "2025-09-19")]

theorem List.Chain.pairwise {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} [Trans R R R] (c : IsChain R l) : Pairwise R l

Alias of List.IsChain.pairwise.

@[deprecated List.Pairwise.isChain (since := "2025-09-24")]

theorem List.Pairwise.chain' {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} (p : Pairwise R l) : IsChain R l

Alias of List.Pairwise.isChain.

@[deprecated List.isChain_iff_pairwise (since := "2025-09-19")]

theorem List.chain_iff_pairwise {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} [Trans R R R] : IsChain R l ↔ Pairwise R l

Alias of List.isChain_iff_pairwise.

@[deprecated List.isChain_iff_pairwise (since := "2025-09-24")]

theorem List.chain'_iff_pairwise {α✝ : Type u_1} {R : α✝ → α✝ → Prop} {l : List α✝} [Trans R R R] : IsChain R l ↔ Pairwise R l

Alias of List.isChain_iff_pairwise.

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

@[deprecated List.IsChain.sublist "Use `IsChain.sublist` combined with `Sublist.cons_cons`" (since := "2025-09-19")]

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

Alias of List.IsChain.sublist.

@[deprecated List.IsChain.sublist (since := "2025-09-24")]

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

Alias of List.IsChain.sublist.

theorem List.IsChain.rel_cons {α : Type u} {R : α → α → Prop} {l : List α} {a b : α} [Trans R R R] (hl : IsChain R (a :: l)) (hb : b ∈ l) : R a b

@[deprecated List.IsChain.rel_cons (since := "2025-09-19")]

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

Alias of List.IsChain.rel_cons.

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

@[deprecated List.IsChain.tail (since := "2025-09-24")]

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

Alias of List.IsChain.tail.

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

@[deprecated List.IsChain.rel_head (since := "2025-09-24")]

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

Alias of List.IsChain.rel_head.

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

@[deprecated List.IsChain.rel_head? (since := "2025-09-24")]

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

Alias of List.IsChain.rel_head?.

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

@[deprecated List.IsChain.cons' (since := "2025-09-24")]

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

Alias of List.IsChain.cons'.

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

@[deprecated List.IsChain.cons_of_ne_nil (since := "2025-09-24")]

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

Alias of List.IsChain.cons_of_ne_nil.

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

@[deprecated List.isChain_cons' (since := "2025-09-24")]

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

Alias of List.isChain_cons'.

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

@[deprecated List.isChain_append (since := "2025-09-24")]

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

Alias of List.isChain_append.

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

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

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

@[deprecated List.isChain_append (since := "2025-09-24")]

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

Alias of List.isChain_append.

@[deprecated List.IsChain.left_of_append (since := "2025-09-24")]

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

Alias of List.IsChain.left_of_append.

@[deprecated List.IsChain.right_of_append (since := "2025-09-24")]

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

Alias of List.IsChain.right_of_append.

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

@[deprecated List.IsChain.infix (since := "2025-09-24")]

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

Alias of List.IsChain.infix.

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

@[deprecated List.IsChain.suffix (since := "2025-09-24")]

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

Alias of List.IsChain.suffix.

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

@[deprecated List.IsChain.prefix (since := "2025-09-24")]

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

Alias of List.IsChain.prefix.

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

@[deprecated List.IsChain.drop (since := "2025-09-24")]

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

Alias of List.IsChain.drop.

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

@[deprecated List.IsChain.dropLast (since := "2025-09-24")]

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

Alias of List.IsChain.dropLast.

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

@[deprecated List.IsChain.take (since := "2025-09-24")]

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

Alias of List.IsChain.take.

theorem List.IsChain.imp_head {α : Type u} {R : α → α → Prop} {x y : α} (h : ∀ {z : α}, R x z → R y z) {l : List α} (hl : IsChain R (x :: l)) : IsChain R (y :: l)

@[deprecated List.IsChain.getElem (since := "2025-09-24")]

theorem List.Chain'.getElem {α : Type u_1} {R : α → α → Prop} {l : List α} (c : IsChain R l) (i : ℕ) (hi : i + 1 < l.length) : R l[i] l[i + 1]

Alias of List.IsChain.getElem.

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

@[deprecated List.isChain_iff_getElem (since := "2025-09-24")]

theorem List.chain'_iff_forall_getElem {α : Type u_1} {R : α → α → Prop} {l : List α} : IsChain R l ↔ ∀ (i : ℕ) (_hi : i + 1 < l.length), R l[i] l[i + 1]

Alias of List.isChain_iff_getElem.

@[deprecated List.isChain_iff_get (since := "2025-09-24")]

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

Alias of List.isChain_iff_get.

theorem List.isChain_cons_iff_get {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : IsChain 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.exists_not_getElem_of_not_isChain {α : Type u} {R : α → α → Prop} {l : List α} (h : ¬IsChain R l) : ∃ (n : ℕ), ∃ (h : n + 1 < l.length), ¬R l[n] l[n + 1]

@[deprecated List.exists_not_getElem_of_not_isChain (since := "2025-09-19")]

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

Alias of List.exists_not_getElem_of_not_isChain.

@[deprecated List.isChain_cons_iff_get (since := "2025-09-19")]

theorem List.chain_iff_get {α : Type u} {R : α → α → Prop} {a : α} {l : List α} : IsChain 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, ⋯⟩)

Alias of List.isChain_cons_iff_get.

theorem List.isChain_reverse {α : Type u} {R : α → α → Prop} {l : List α} : IsChain R l.reverse ↔ IsChain (flip R) l

@[deprecated List.isChain_reverse (since := "2025-09-24")]

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

Alias of List.isChain_reverse.

theorem List.IsChain.append_overlap {α : Type u} {R : α → α → Prop} {l₁ l₂ l₃ : List α} (h₁ : IsChain R (l₁ ++ l₂)) (h₂ : IsChain R (l₂ ++ l₃)) (hn : l₂ ≠ []) : IsChain R (l₁ ++ l₂ ++ l₃)

If l₁ l₂ and l₃ are lists and l₁ ++ l₂ and l₂ ++ l₃ both satisfy IsChain R, then so does l₁ ++ l₂ ++ l₃ provided l₂ ≠ []

@[deprecated List.IsChain.append_overlap (since := "2025-09-24")]

theorem List.Chain'.append_overlap {α : Type u} {R : α → α → Prop} {l₁ l₂ l₃ : List α} (h₁ : IsChain R (l₁ ++ l₂)) (h₂ : IsChain R (l₂ ++ l₃)) (hn : l₂ ≠ []) : IsChain R (l₁ ++ l₂ ++ l₃)

Alias of List.IsChain.append_overlap.

---

If l₁ l₂ and l₃ are lists and l₁ ++ l₂ and l₂ ++ l₃ both satisfy IsChain R, then so does l₁ ++ l₂ ++ l₃ provided l₂ ≠ []

theorem List.isChain_flatten {α : Type u} {R : α → α → Prop} {L : List (List α)} : ¬[] ∈ L → (IsChain R L.flatten ↔ (∀ (l : List α), l ∈ L → IsChain R l) ∧ IsChain (fun (l₁ l₂ : List α) => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) L)

@[deprecated List.isChain_flatten (since := "2025-09-24")]

theorem List.chain'_flatten {α : Type u} {R : α → α → Prop} {L : List (List α)} : ¬[] ∈ L → (IsChain R L.flatten ↔ (∀ (l : List α), l ∈ L → IsChain R l) ∧ IsChain (fun (l₁ l₂ : List α) => ∀ (x : α), x ∈ l₁.getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) L)

Alias of List.isChain_flatten.

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

@[deprecated List.isChain_attachWith (since := "2025-09-24")]

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

Alias of List.isChain_attachWith.

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

@[deprecated List.isChain_attach (since := "2025-09-24")]

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

Alias of List.isChain_attach.

theorem List.exists_isChain_cons_of_relationReflTransGen {α : Type u} {r : α → α → Prop} {a b : α} (h : Relation.ReflTransGen r a b) : ∃ (l : List α), IsChain 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.

@[deprecated List.exists_isChain_cons_of_relationReflTransGen (since := "2025-09-22")]

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

Alias of List.exists_isChain_cons_of_relationReflTransGen.

---

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.

theorem List.exists_isChain_ne_nil_of_relationReflTransGen {α : Type u} {r : α → α → Prop} {a b : α} (h : Relation.ReflTransGen r a b) : ∃ (l : List α), ∃ (hl : l ≠ []), IsChain r l ∧ l.head hl = a ∧ l.getLast hl = 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.

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

Given a chain l, such that a predicate p holds for its head if it is nonempty, and 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.

@[deprecated List.IsChain.induction (since := "2025-09-24")]

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

Alias of List.IsChain.induction.

---

Given a chain l, such that a predicate p holds for its head if it is nonempty, and 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.IsChain.cons_induction {α : Type u} {r : α → α → Prop} {a : α} (p : α → Prop) (l : List α) (h : IsChain 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.

@[deprecated List.IsChain.cons_induction (since := "2025-09-24")]

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

Alias of List.IsChain.cons_induction.

---

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.IsChain.concat_induction {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b])) (hb : (l ++ [b]).head ⋯ = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) (i : α) : i ∈ l ++ [b] → p i

theorem List.IsChain.concat_induction_head {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b])) (hb : (l ++ [b]).head ⋯ = a) (carries : ∀ ⦃x y : α⦄, r x y → p x → p y) (initial : p a) : p b

theorem List.IsChain.backwards_induction {α : Type u} {r : α → α → Prop} (p : α → Prop) (l : List α) (h : IsChain r l) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : ∀ (lne : l ≠ []), p (l.getLast lne)) (i : α) : i ∈ 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.IsChain.backwards_concat_induction {α : Type u} {r : α → α → Prop} {b : α} (p : α → Prop) (l : List α) (h : IsChain r (l ++ [b])) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) (i : α) : i ∈ 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.IsChain.backwards_cons_induction {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain 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

@[deprecated List.IsChain.backwards_cons_induction (since := "2025-09-24")]

theorem List.Chain.backwards_induction {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain 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

Alias of List.IsChain.backwards_cons_induction.

theorem List.IsChain.backwards_cons_induction_head {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain 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.

@[deprecated List.IsChain.backwards_cons_induction_head (since := "2025-09-24")]

theorem List.Chain.backwards_induction_head {α : Type u} {r : α → α → Prop} {a b : α} (p : α → Prop) (l : List α) (h : IsChain r (a :: l)) (hb : (a :: l).getLast ⋯ = b) (carries : ∀ ⦃x y : α⦄, r x y → p y → p x) (final : p b) : p a

Alias of List.IsChain.backwards_cons_induction_head.

---

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_isChain {α : Type u} {r : α → α → Prop} (l : List α) (hl₁ : IsChain r l) (hne : l ≠ []) : Relation.ReflTransGen r (l.head hne) (l.getLast hne)

If there is an non-empty r-chain, its head and last element are related by the reflexive transitive closure of r.

theorem List.relationReflTransGen_of_exists_isChain_cons {α : Type u} {r : α → α → Prop} {a b : α} (l : List α) (hl₁ : IsChain 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.

@[deprecated List.relationReflTransGen_of_exists_isChain_cons (since := "2025-09-24")]

theorem List.relationReflTransGen_of_exists_chain_cons {α : Type u} {r : α → α → Prop} {a b : α} (l : List α) (hl₁ : IsChain r (a :: l)) (hl₂ : (a :: l).getLast ⋯ = b) : Relation.ReflTransGen r a b

Alias of List.relationReflTransGen_of_exists_isChain_cons.

---

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.

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

@[deprecated List.IsChain.cons_of_le (since := "2025-09-24")]

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

Alias of List.IsChain.cons_of_le.

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

@[deprecated List.IsChain.isChain_cons (since := "2025-09-24")]

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

Alias of List.IsChain.isChain_cons.

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

@[deprecated List.IsChain.iterate_eq_of_apply_eq (since := "2025-09-24")]

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

Alias of List.IsChain.iterate_eq_of_apply_eq.

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

@[deprecated List.isChain_replicate_of_rel "Use `isChain_replicate_of_rel` with `n + 1` instead" (since := "2025-09-19")]

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

Alias of List.isChain_replicate_of_rel.

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

@[deprecated List.isChain_eq_iff_eq_replicate (since := "2025-09-19")]

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

Alias of List.isChain_eq_iff_eq_replicate.

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

@[deprecated List.isChain_cons_eq_iff_eq_replicate (since := "2025-09-19")]

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

Alias of List.isChain_cons_eq_iff_eq_replicate.

In this section, we consider the type of r-decreasing chains (List.IsChain (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.IsChain (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)