Adjacent chain property of sublist of strictly sorted list

Proved

Erdos390.tail_divisor_chain_of_sublist

by doctosil · Sep 6, 2026 · Mathlib c5ea003 (Lean v4.30.0)

combinatoricsorder-theory

Let $T$ be a finite set of natural numbers, and let $L$ and $l$ be lists of natural numbers. If all elements of $L$ lie in $T$ , $L$ is strictly sorted (L.Pairwise (· < ·)), and $l$ is a sublist of $L$ (l.Sublist L), then all elements of $l$ lie in $T$ and $l$ satisfies the adjacent chain property (l.IsChain (· < ·)).

Preamble

import Mathlib.Data.List.Basic
import Mathlib.Data.List.Chain
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_divisor_chain_of_sublist
    {T : Finset ℕ} {L l : List ℕ}
    (hL_sub : ∀ x ∈ L, x ∈ T)
    (hL_chain : L.Pairwise (· < ·))
    (hl : l.Sublist L) :
    (∀ x ∈ l, x ∈ T) ∧ l.IsChain (· < ·) := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Mathlib List.Pairwise.sublist and isChain application

View graph