Pair sublist inclusion and binary factor evaluation

Proved

Erdos390.tail_divisor_pair_sublist

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

combinatoricsorder-theory

Let $L$ be a strictly ascending list of natural numbers (L.Pairwise (· < ·)), and let $a, b \in \mathbb{N}$ satisfy $a \in L$ , $b \in L$ , and $a < b$ . Then the two-element list $[a, b]$ is a sublist of $L$ (List.Sublist [a, b] L), and its product is $a \cdot b$ (List.prod [a, b] = a * b).

Preamble

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

Formal statement

namespace Erdos390

theorem tail_divisor_pair_sublist
    {L : List ℕ} {a b : ℕ}
    (hL : L.Pairwise (· < ·))
    (ha : a ∈ L) (hb : b ∈ L) (hab : a < b) :
    List.Sublist [a, b] L ∧ List.prod [a, b] = a * b := by sorry

end Erdos390

Source

P. Erdős, Some problems in number theory, 1975; Mathlib List.Sublist constructors

View graph