Pairwise strict ordering from adjacent chain condition

Proved

Erdos390.tail_divisor_pairwise_of_chain

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

combinatoricsorder-theory

Let $l$ be a list of natural numbers. If $l$ satisfies the adjacent chain condition (l.IsChain (· < ·)), then $l$ satisfies global pairwise ordering (l.Pairwise (· < ·)).

Preamble

import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_divisor_pairwise_of_chain
    {l : List ℕ}
    (hchain : l.IsChain (· < ·)) :
    l.Pairwise (· < ·) := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Mathlib List.isChain_iff_pairwise application

View graph