Arithmetic progression
ContainsAPOfLengthdef
A set of naturals contains an arithmetic progression of length k when some a and positive common difference d place all of a, a+d, …, a+(k-1)d inside it.
def ContainsAPOfLength (S : Set ℕ) (k : ℕ) : Prop :=
∃ a d : ℕ, 0 < d ∧ ∀ i < k, a + i * d ∈ SFrom Mathlib
import Conjectura.Defs.Mathematics.Combinatorics.ArithmeticProgression · maintainer — open · raw source
Copyright (c) 2026 The Conjectura Authors. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: The Conjectura Authors