Duplicate-free property of strictly sorted list

Proved

Erdos390.tail_divisor_nodup_of_sorted

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

combinatoricsorder-theory

Let $l$ be a list of natural numbers. If $l$ is strictly sorted (l.Pairwise (· < ·)), then $l$ has no duplicate elements (l.Nodup).

Preamble

import Mathlib
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem tail_divisor_nodup_of_sorted
    (l : List ℕ)
    (hsorted : l.Pairwise (· < ·)) :
    l.Nodup := by sorry

end Erdos390

Source

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