Support and strict ordering of canonical consecutive tail list

Proved

Erdos390.canonical_tail_list_spec

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

combinatoricsorder-theory

Let $n, h \in \mathbb{N}$ . The consecutive range list $L = \mathrm{List.range'} (2n + 1) h = [2n + 1, \dots, 2n + h]$ satisfies:

\left(\forall x \in L, \; x \in (2n, 2n + h]\right) \quad \wedge \quad L.\mathrm{Pairwise}(<).

Preamble

import Mathlib.Data.List.Range
import Mathlib.Data.Finset.Interval
import Definitions.Def_erdos390_problem
open Erdos390

Formal statement

namespace Erdos390

theorem canonical_tail_list_spec (n h : ℕ) :
    let L := List.range' (2 * n + 1) h
    (∀ x ∈ L, x ∈ factorInterval (2 * n) (2 * n + h)) ∧ L.Pairwise (· < ·) := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Mathlib List.pairwise_lt_range' and List.mem_range'

View graph