def Kreis_in_Kugel : Set r_3

Equations

• Kreis_in_Kugel = {p : r_3 | (2 * p 0 + 1) ^ 2 + (2 * p 1) ^ 2 = 1 ∧ p 2 = 0 ∧ -p 0 ≤ 1}

def Kreis_in_Kugel_ohne_Origin : Set r_3

Equations

• Kreis_in_Kugel_ohne_Origin = Kreis_in_Kugel \ {origin}

def Part_B : Set r_3

Equations

• Part_B = L' \ Kreis_in_Kugel_ohne_Origin

def Kreis_in_Kugel_A : Set r_3

Equations

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

def Kreis_in_Kugel_B : Set r_3

Equations

• Kreis_in_Kugel_B = Kreis_in_Kugel_ohne_Origin \ Kreis_in_Kugel_A

theorem Kreis_subset_L : Kreis_in_Kugel ⊆ L

theorem Part_B_union_Kreis_in_Kugel_eq_L : Part_B ∪ Kreis_in_Kugel = L

theorem Part_B_and_Kreis_in_Kugel_ohne_origin_eq_L' : Part_B ∪ Kreis_in_Kugel_ohne_Origin = L'

theorem intersection_Part_B_Kreis_in_Kugel_ohne_Origin_eq_nil : Part_B ∩ Kreis_in_Kugel_ohne_Origin = ∅

theorem union_A_B_eq_Kreis : list_union [Kreis_in_Kugel_A, Kreis_in_Kugel_B] = Kreis_in_Kugel_ohne_Origin

theorem intersection_A_B_eq_nil : Kreis_in_Kugel_A ∩ Kreis_in_Kugel_B = ∅

theorem le_lemma (n : ℕ) : Real.sin (↑n * sq_2) * Real.sin sq_2 * (-1 / 2) ≤ 1 / 2 + Real.cos (↑n * sq_2) * Real.cos sq_2 * (1 / 2)

theorem equi_kreis_in_kugel_aux : {w : r_3 | ∃ a ∈ Kreis_in_Kugel_A, translate ![-1 / 2, 0, 0] (rotate gl_sq_2 (translate ![2⁻¹, 0, 0] a)) = w} ∪ {w : r_3 | ∃ v ∈ Kreis_in_Kugel_B, rotate 1 v = w} = Kreis_in_Kugel

theorem equi_kreis_in_kugel : equidecomposable Kreis_in_Kugel_ohne_Origin Kreis_in_Kugel

theorem equi_kugel : equidecomposable L' L