lean_workbook_plus_18918

Proved

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

Let $n$ be a positive integer. Let $A = \{1,2 \dots, 2n \}, S \subset A$ with $n+1$ elements. Show there exist two elements of $S$ , one of which divides the other.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18918 (n : ℕ) (hn : 0 < n) (A : Finset ℕ) (hA : A = Finset.Icc 1 (2 * n)) (S : Finset ℕ) (hS : S ⊆ A) (hS' : n + 1 ≤ S.card) : ∃ x ∈ S, ∃ y ∈ S, x ∣ y   :=  by sorry

Source

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

View graph