# 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.

source
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
source
theorem List.isChain_nil {α : Type u} {R : α → α → Prop} :
IsChain R []
source
theorem List.isChain_singleton {α : Type u} {R : α → α → Prop} (a : α) :
IsChain R [a]
source
@[deprecated List.isChain_nil (since := "2025-09-24")]
theorem List.chain'_nil {α : Type u} {R : α → α → Prop} :
IsChain R []

Alias of `List.isChain_nil`.

source
@[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`.

source
@[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`.

source
@[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`.

source
@[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

Instances For

source
@[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

Instances For

source
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'
source
@[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`.

source
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
source
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
source
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
source
@[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`.

source
@[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`.

source
@[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`.

source
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
source
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
source
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
source
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
source
@[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`.

source
@[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`.

source
theorem List.isChain_pair {α : Type u} {R : α → α → Prop} {x y : α} :
IsChain R [x, y] ↔ R x y
source
@[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`.

source
@[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`.

source
theorem List.isChain_isInfix {α : Type u} (l : List α) :
IsChain (fun (x y : α) => [x, y] <:+: l) l
source
@[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`.

source
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₂)
source
@[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`.

source
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₂)
source
@[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`.

source
@[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₂)
source
@[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`.

source
@[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₂)
source
@[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`.

source
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
source
@[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`.

source
theorem List.isChain_iff_forall₂ {α : Type u} {R : α → α → Prop} {l : List α} :
IsChain R l ↔ Forall₂ R l.dropLast l.tail
source
theorem List.isChain_cons_iff_forall₂ {α : Type u} {R : α → α → Prop} {l : List α} {a : α} :
IsChain R (a :: l) ↔ l = [] ∨ Forall₂ R (a :: l.dropLast) l
source
@[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₂`.

source
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])
source
@[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₂`.

source
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
source
@[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`.

source
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
source
@[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`.

source
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)
source
@[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`.

source
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)
source
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)
source
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)
source
@[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`.

source
@[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`.

source
@[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`.

source
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
source
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₂)
source
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
source
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)
source
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₂)
source
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)
source
@[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`.

source
@[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`.

source
@[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`.

source
@[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`.

source
@[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`.

source
@[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`.

source
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₁
source
@[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`.

source
@[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`.

source
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
source
@[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`.

source
theorem List.IsChain.of_cons {α : Type u} {R : α → α → Prop} {x : α} {l : List α} :
IsChain R (x :: l) → IsChain R l
source
theorem List.IsChain.tail {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) :
IsChain R l.tail
source
@[deprecated List.IsChain.tail (since := "2025-09-24")]
theorem List.Chain'.tail {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) :
IsChain R l.tail

Alias of `List.IsChain.tail`.

source
theorem List.IsChain.rel_head {α : Type u} {R : α → α → Prop} {x y : α} {l : List α} (h : IsChain R (x :: y :: l)) :
R x y
source
@[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`.

source
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
source
@[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?`.

source
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)
source
@[deprecated List.IsChain.cons (since := "2025-10-16")]
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)

Alias of `List.IsChain.cons`.

source
@[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`.

source
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)
source
@[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`.

source
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
source
@[deprecated List.isChain_cons (since := "2025-10-16")]
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

Alias of `List.isChain_cons`.

source
@[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`.

source
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
source
@[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`.

source
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₂)
source
theorem List.IsChain.left_of_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} (h : IsChain R (l₁ ++ l₂)) :
IsChain R l₁
source
theorem List.IsChain.right_of_append {α : Type u} {R : α → α → Prop} {l₁ l₂ : List α} (h : IsChain R (l₁ ++ l₂)) :
IsChain R l₂
source
@[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`.

source
@[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`.

source
@[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`.

source
theorem List.IsChain.infix {α : Type u} {R : α → α → Prop} {l l₁ : List α} (h : IsChain R l) (h' : l₁ <:+: l) :
IsChain R l₁
source
@[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`.

source
theorem List.IsChain.suffix {α : Type u} {R : α → α → Prop} {l l₁ : List α} (h : IsChain R l) (h' : l₁ <:+ l) :
IsChain R l₁
source
@[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`.

source
theorem List.IsChain.prefix {α : Type u} {R : α → α → Prop} {l l₁ : List α} (h : IsChain R l) (h' : l₁ <+: l) :
IsChain R l₁
source
@[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`.

source
theorem List.IsChain.drop {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) (n : ℕ) :
IsChain R (List.drop n l)
source
@[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`.

source
theorem List.IsChain.dropLast {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) :
IsChain R l.dropLast
source
@[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`.

source
theorem List.IsChain.take {α : Type u} {R : α → α → Prop} {l : List α} (h : IsChain R l) (n : ℕ) :
IsChain R (List.take n l)
source
@[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`.

source
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)
source
@[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`.

source
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⟩)
source
@[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`.

source
@[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`.

source
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, ⋯⟩)
source
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]
source
@[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`.

source
@[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`.

source
theorem List.isChain_reverse {α : Type u} {R : α → α → Prop} {l : List α} :
IsChain R l.reverse ↔ IsChain (flip R) l
source
@[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`.

source
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₂ ≠ []`

source
@[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₂ ≠ []`

source
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)
source
@[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`.

source
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
source
@[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`.

source
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
source
@[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`.

source
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`.

source
@[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`.

source
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`.

source
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.

source
@[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.

source
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.

source
@[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.

source
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
source
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
source
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.

source
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.

source
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
source
@[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`.

source
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.

source
@[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.

source
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`.

source
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`.

source
@[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`.

source
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)
source
@[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`.

source
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)
source
@[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`.

source
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]
source
@[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`.

source
theorem List.isChain_replicate_of_rel {α : Type u} {r : α → α → Prop} (n : ℕ) {a : α} (h : r a a) :
IsChain r (replicate n a)
source
@[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`.

source
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
source
@[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`.

source
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
source
@[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`.

source
@[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 }

Instances For

source
@[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

Instances For

source
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`.

source
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.

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