def S : Set r_3

Equations

• S = {x : r_3 | x 2 = 0 ∧ x 0 ^ 2 + x 1 ^ 2 = 1}

def A : Set r_3

Equations

• A = {w : r_3 | ∃ (n : ↑{x : ℕ | x > 0}), w = ![Real.cos (↑↑n * sq_2), Real.sin (↑↑n * sq_2), 0]}

def B : Set r_3

Equations

• B = (S \ {![1, 0, 0]}) \ A

theorem A_and_B_eq_S : A ∪ B = S \ {![1, 0, 0]}

theorem rotate_A_B_eq_S : rotate_set A gl_sq_2 ∪ rotate_set B gl_one = S

theorem equi_kreis : equidecomposable (S \ {![1, 0, 0]}) S