Triple sublist inclusion and ternary factor evaluation

Proved

Erdos390.tail_divisor_triple_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, c \in \mathbb{N}$ satisfy $a \in L$ , $b \in L$ , $c \in L$ , and $a < b < c$ . Then the three-element list $[a, b, c]$ is a sublist of $L$ (List.Sublist [a, b, c] L), and its product is $a \cdot b \cdot c$ (List.prod [a, b, c] = a * b * c).

Preamble

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

Formal statement

namespace Erdos390

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

end Erdos390

Source

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

View graph