Gordon’s Conjectures 1 and 2: Pontryagin–van Kampen duality in the hyperfinite setting

PAVOL ZLATOSˇ

Proposition 2.1.3 concerns the set D - D. Here we define in general A + B.

instance instHAddSetOfAdd_marginis (X : Type) [Add X] : HAdd (Set X) (Set X) (Set X)

Equations

• instHAddSetOfAdd_marginis X = { hAdd := fun (A B : Set X) (x : X) => ∃ (y : X), ∃ (z : X), y ∈ A ∧ z ∈ B ∧ x = y + z }

theorem add_example : {x : ℕ | x ≤ 1} + {x : ℕ | x ≥ 2} = {x : ℕ | x ≥ 2}