/-
Copyright 2025 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilErdős Problem 949
open Cardinal Filteropen scoped Pointwise Topology
namespace Erdos949
Let $S \subseteq \mathbb{R}$ be a set containing no solutions to $a + b = c$. Must there be a set $A \subseteq \mathbb{R} \setminus S$ of cardinality continuum such that $A + A \subseteq \mathbb{R}\setminus S$?
@[category research open, AMS 5]
theorem erdos_949 : answer(sorry) ↔
∀ S : Set ℝ, (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ := ⊢ True ↔ ∀ (S : Set ℝ), (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ Sᶜ
All goals completed! 🐙Let $S\sub \mathbb{R}$ be a Sidon set. Must there be a set $A\sub \mathbb{R}∖S$ of cardinality continuum such that $A + A \sub \mathbb{R}∖S$?
@[category research solved, AMS 5, formal_proof using formal_conjectures at ""]
theorem erdos_949.variants.sidon : answer(True) ↔
∀ S : Set ℝ, IsSidon S → ∃ A ⊆ Sᶜ, #A = 𝔠 ∧ A + A ⊆ Sᶜ := ⊢ True ↔ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ Sᶜ
⊢ True ↔ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ Sᶜ
⊢ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
S:Set ℝhS:IsSidon S⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
-- We case on whether `S` has cardinality the continuum or strictly less.
obtain hS𝔠 | hS𝔠 : #S < 𝔠 ∨ #S = 𝔠 := lt_or_eq_of_le <| S:Set ℝhS:IsSidon S⊢ #↑S ≤ 𝔠 All goals completed! 🐙
-- If `S` has cardinality strictly less than the continuum, then we pick by Zorn `A` maximal
-- such that both `A` and `A + A` are disjoint from `S`.
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ obtain ⟨A, ⟨hAS, hAAS⟩, hAmax⟩ := S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ?m.63
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∀ c ⊆ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S},
IsChain (fun x1 x2 => x1 ⊆ x2) c → ∃ ub ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}, ∀ s ∈ c, s ⊆ ub
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠⊢ ∀ c ⊆ {a | a ⊆ Sᶜ},
c ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S} →
IsChain (fun x1 x2 => x1 ⊆ x2) c → ∃ ub ⊆ Sᶜ, (∀ x ∈ ub, ∀ y ∈ ub, x + y ∉ S) ∧ ∀ s ∈ c, s ⊆ ub
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 => x1 ⊆ x2) C⊢ ∀ x ∈ ⋃ i ∈ C, i, ∀ y ∈ ⋃ i ∈ C, i, x + y ∉ S
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 => x1 ⊆ x2) C⊢ ∀ (x : ℝ), ∀ x_1 ∈ C, x ∈ x_1 → ∀ (y : ℝ), ∀ x_2 ∈ C, y ∈ x_2 → x + y ∉ S
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 => x1 ⊆ x2) Cx:ℝA:Set ℝhA:A ∈ Chx:x ∈ Ay:ℝB:Set ℝhB:B ∈ Chy:y ∈ B⊢ x + y ∉ S
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠C:Set (Set ℝ)hCS:C ⊆ {a | a ⊆ Sᶜ}hSC:C ⊆ {a | ∀ x ∈ a, ∀ y ∈ a, x + y ∉ S}hC:IsChain (fun x1 x2 => x1 ⊆ x2) Cx:ℝA:Set ℝhA:A ∈ Chx:x ∈ Ay:ℝB:Set ℝhB:B ∈ Chy:y ∈ BD:Set ℝhD:D ∈ ChAD:A ⊆ DhBD:B ⊆ D⊢ x + y ∉ S
All goals completed! 🐙
-- By construction, `A` satisfies all properties except possibly for having size the continuum.
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ≤ y → y ≤ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ #↑A = 𝔠
-- By maximality, `Sᶜ ∩ (S / 2)ᶜ ⊆ A ∪ ⋃ a ∈ A, (S - a)`.
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ≤ y → y ≤ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' SS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S⊢ #↑A = 𝔠
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ≤ y → y ≤ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ≤ y → y ≤ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ S⊢ ∀ x ∉ S, x + x ∉ S → x ∉ A → ∃ i ∈ A, x + i ∈ S
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ≤ y → y ≤ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ Sx:ℝhxS:x ∉ ShxxS:x + x ∉ ShxA:x ∉ A⊢ ∃ i ∈ A, x + i ∈ S
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ≤ y → y ≤ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ Sx:ℝhxS:x ∉ ShxxS:x + x ∉ ShxA:x ∉ AhxAS:∀ i ∈ A, x + i ∉ S⊢ False
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAmax:∀ ⦃y : Set ℝ⦄, (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) y → A ≤ y → y ≤ AhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ Sx:ℝhxS:x ∉ ShxxS:x + x ∉ ShxA:x ∉ AhxAS:∀ i ∈ A, x + i ∉ S⊢ (fun x => x ∈ {A | A ⊆ Sᶜ ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∉ S}) (insert x A)
All goals completed! 🐙
-- By assumption, `#(Sᶜ ∩ (S / 2)ᶜ) = 𝔠`.
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S⊢ #↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠⊢ #↑A = 𝔠
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S⊢ #↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠 S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S⊢ #↑(S ∪ (fun x => x / 2) '' S) < #ℝ
grw [mk_union_le, Cardinal.mk_realS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S⊢ #↑S + #↑((fun x => x / 2) '' S) < 𝔠
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S⊢ #↑((fun x => x / 2) '' S) < 𝔠
grw [mk_image_leS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' S⊢ #↑S < 𝔠
All goals completed! 🐙
-- If `#A < 𝔠`, we would then have
-- `𝔠 = #(Sᶜ ∩ (S / 2)ᶜ) ≤ #(A ∪ ⋃ a ∈ A, (S - a)) ≤ #A + #A * #S < 𝔠`, contradiction.
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠⊢ 𝔠 < 𝔠
calc
𝔠 = #↑(Sᶜ ∩ ((· / 2) '' S)ᶜ) := S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠⊢ 𝔠 = #↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) All goals completed! 🐙
_ ≤ #↑(A ∪ ⋃ a ∈ A, (· - a) '' S) := mk_subtype_mono hAmax
_ ≤ #A + #A * #S := S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠⊢ #↑(A ∪ ⋃ a ∈ A, (fun x => x - a) '' S) ≤ #↑A + #↑A * #↑S
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠hS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠hAS:∅ ⊆ SᶜhAAS:∀ x ∈ ∅, ∀ y ∈ ∅, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ ∅ ∪ ⋃ a ∈ ∅, (fun x => x - a) '' ShA𝔠:#↑∅ < 𝔠⊢ #↑(∅ ∪ ⋃ a ∈ ∅, (fun x => x - a) '' S) ≤ #↑∅ + #↑∅ * #↑SS:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠hA:A.Nonempty⊢ #↑(A ∪ ⋃ a ∈ A, (fun x => x - a) '' S) ≤ #↑A + #↑A * #↑S
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠hS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠hAS:∅ ⊆ SᶜhAAS:∀ x ∈ ∅, ∀ y ∈ ∅, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ ∅ ∪ ⋃ a ∈ ∅, (fun x => x - a) '' ShA𝔠:#↑∅ < 𝔠⊢ #↑(∅ ∪ ⋃ a ∈ ∅, (fun x => x - a) '' S) ≤ #↑∅ + #↑∅ * #↑S All goals completed! 🐙
S:Set ℝhS:IsSidon ShS𝔠:#↑S < 𝔠A:Set ℝhAS:A ⊆ SᶜhAAS:∀ x ∈ A, ∀ y ∈ A, x + y ∉ ShAmax:Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ ⊆ A ∪ ⋃ a ∈ A, (fun x => x - a) '' ShS𝔠':#↑(Sᶜ ∩ ((fun x => x / 2) '' S)ᶜ) = 𝔠hA𝔠:#↑A < 𝔠hA:A.Nonemptythis:Nonempty ↑A := Set.Nonempty.coe_sort hA⊢ #↑(A ∪ ⋃ a ∈ A, (fun x => x - a) '' S) ≤ #↑A + #↑A * #↑S
grw [mk_union_le, mk_biUnion_le, ciSup_le fun _ ↦ mk_image_leAll goals completed! 🐙
_ < 𝔠 := add_lt_of_lt aleph0_le_continuum hA𝔠 <| mul_lt_of_lt aleph0_le_continuum hA𝔠 hS𝔠
-- If `S` has cardinality the continuum, then we pick some `a ≠ 0` in `S` and set
-- `A := (S \ {a} - a / 2) \ S`.
have hSinf : S.Infinite := ⊢ True ↔ ∀ (S : Set ℝ), IsSidon S → ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ A + A ⊆ Sᶜ All goals completed! 🐙
S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ ∃ A ⊆ Sᶜ, #↑A = 𝔠 ∧ ∀ x ∈ A, ∀ y ∈ A, x + y ∈ Sᶜ
S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun x => x - a / 2) '' (S \ {a}) \ S) = 𝔠S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ ∀ x ∈ (fun x => x - a / 2) '' (S \ {a}) \ S, ∀ y ∈ (fun x => x - a / 2) '' (S \ {a}) \ S, x + y ∈ Sᶜ
-- Since `S` is Sidon and `a ≠ 0`, `(S - a / 2) ∩ S ⊇ (S \ {a} - a / 2) ∩ S` has at most one
-- element. In particular, `#A = #(S \ {a} - a / 2) = #S = 𝔠` as wanted.
S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun x => x - a / 2) '' (S \ {a}) \ S) = 𝔠 S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun a_1 => a_1 - a / 2) '' (S \ {a})) = 𝔠S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 => a_1 - a / 2) '' (S \ {a}) ∩ S).Finite
S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ #↑((fun a_1 => a_1 - a / 2) '' (S \ {a})) = 𝔠 All goals completed! 🐙
S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 => a_1 - a / 2) '' (S \ {a}) ∩ S).Finite S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ ((fun a_1 => a_1 - a / 2) '' (S \ {a}) ∩ S).Subsingleton
S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 => a_1 - a / 2) x ∈ Sy:ℝhy:y ∈ Shya:(fun a_1 => a_1 - a / 2) y ∈ S⊢ (fun a_1 => a_1 - a / 2) x = (fun a_1 => a_1 - a / 2) y
obtain rfl : x = y := S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 => a_1 - a / 2) x ∈ Sy:ℝhy:y ∈ Shya:(fun a_1 => a_1 - a / 2) y ∈ S⊢ x = y
simpa [ha₀, eq_comm (b := x - _)] using hS _ hya _ hxa _ hx _ hy (S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:(fun a_1 => a_1 - a / 2) x ∈ Sy:ℝhy:y ∈ Shya:(fun a_1 => a_1 - a / 2) y ∈ S⊢ (fun a_1 => a_1 - a / 2) y + x = (fun a_1 => a_1 - a / 2) x + y All goals completed! 🐙)
All goals completed! 🐙
-- Since `S` is Sidon, `S \ {a} + S \ {a} - a ⊇ A + A` is disjoint from `S`, as wanted.
S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0⊢ ∀ x ∈ (fun x => x - a / 2) '' (S \ {a}) \ S, ∀ y ∈ (fun x => x - a / 2) '' (S \ {a}) \ S, x + y ∈ Sᶜ S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:x ∉ {a}y:ℝhy:y ∈ Shya:y ∉ {a}hxy:(fun x => x - a / 2) x + (fun x => x - a / 2) y ∈ S⊢ False
have := hS _ hx _ ha _ hy _ hxy (S:Set ℝhS:IsSidon ShS𝔠:#↑S = 𝔠hSinf:S.Infinite := Eq.mp aleph0_le_mk_set._simp_1 (LE.le.trans_eq aleph0_le_continuum (Eq.symm hS𝔠))a:ℝha:a ∈ Sha₀:a ≠ 0x:ℝhx:x ∈ Shxa:x ∉ {a}y:ℝhy:y ∈ Shya:y ∉ {a}hxy:(fun x => x - a / 2) x + (fun x => x - a / 2) y ∈ S⊢ x + y = a + ((fun x => x - a / 2) x + (fun x => x - a / 2) y) All goals completed! 🐙)
All goals completed! 🐙
end Erdos949