def IsSidon {ι : Type u_1} {α : Type u_2} [Preorder ι] [Preorder α] [Add α] (a : ι →o α) : Prop

A Sidon sequence (also called a Sidon set) is a sequence of natural numbers $a_0, a_1, ...$ such that all pairwise sums $a_i + a_j$ are distinct for $i ≤ j$.

In other words, all pairwise sums of elements are distinct apart from coincidences forced by the commutativity of addition.

Equations

• IsSidon a = ∀ (i₁ j₁ i₂ j₂ : ι), i₁ ≤ j₁ → i₂ ≤ j₂ → a i₁ + a j₁ = a i₂ + a j₂ → i₁ = i₂ ∧ j₁ = j₂

theorem IsSidon.injective {ι : Type u_1} {α : Type u_2} [Preorder ι] [Preorder α] [Add α] (a : ι →o α) (ha : IsSidon a) : Function.Injective ⇑a

def Set.IsAPOfLength {α : Type u_1} [AddCommMonoid α] (s : Set α) (l : ℕ∞) : Prop

The predicate that a set s is an arithmetic progression of length l (possibly infinite).

Equations

• s.IsAPOfLength l = ∃ (a : α) (d : α), d ≠ 0 ∧ s = {x : α | ∃ (n : ℕ) (_ : ↑n < l), a + n • d = x}

theorem Set.IsAPOfLength.card {α : Type u_1} [AddCommMonoid α] (s : Set α) (l : ℕ∞) (hs : s.IsAPOfLength l) : ENat.card ↑s = l

theorem IsSidon.avoids_isAPOfLength_three {α : Type u_2} [OrderedAddCommMonoid α] (A : ℕ →o α) (hA : IsSidon A) (Y : Set α) : Y.IsAPOfLength 3 → (Set.range ⇑A ∩ Y).ncard ≤ 2