lean_workbook_plus_78361

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Generalisation: between any $n+1$ numbers from $\{1,2,\cdots ,2n\}$ we can find two elements $a,b$ such that $a\mid b$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78361 (n : ℕ) (A : Finset ℕ) (hA : A.card = n + 1) (hA2 : ∀ a ∈ A, a ∈ Finset.Icc 1 (2 * n)) : ∃ a b, a ∈ A ∧ b ∈ A ∧ a ∣ b   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph