def intersection {α : Type} (a : Set α × Set α) : Set α

Equations

• intersection a = a.1 ∩ a.2

def union {α : Type} (a : Set α) (b : Set α) : Set α

Equations

• union a b = a ∪ b

def list_union {α : Type} (x : List (Set α)) : Set α

Equations

• list_union x = List.foldl union ∅ x

def pairs {α : Type u_1} : List α → List (α × α)

Equations

• pairs [] = []
• pairs (x_1 :: xs) = List.map (fun (y : α) => (x_1, y)) xs ++ pairs xs

def list_intersection {α : Type} (x : List (Set α)) : Set α

Equations

• list_intersection x = list_union (List.map intersection (pairs x))

def translate_set (x : Set r_3) (p : r_3) : Set r_3

Equations

• translate_set x p = {w : r_3 | ∃ v ∈ x, translate p v = w}

theorem translate_zero (x : r_3) : translate ![0, 0, 0] x = x

theorem translate_set_zero (x : Set r_3) : translate_set x ![0, 0, 0] = x

def remove_first {α : Type} (x : List α) : List α

Equations

• remove_first x = List.tail x

theorem remove_first_length_eq {α : Type} {a : Type} {n : ℕ} (x : List α) (h_n : n = List.length x) : List.length (remove_first x) = n - 1

def rotate_list (n : ℕ) (x : List (Set r_3)) (p : List (GL (Fin 3) ℝ)) (h_n : n = List.length x) (h : List.length x = List.length p) : List (Set r_3)

Equations

• One or more equations did not get rendered due to their size.
• rotate_list 0 x p h_n_2 h = []

theorem rotate_list_length_cons (n : ℕ) (x : List (Set r_3)) (p : List (GL (Fin 3) ℝ)) (h_n : n = List.length x) (h : List.length x = List.length p) : List.length (rotate_list n x p h_n h) = n

def translate_list (n : ℕ) (x : List (Set r_3)) (p : List r_3) (h_n : n = List.length x) (h : List.length x = List.length p) : List (Set r_3)

Equations

• One or more equations did not get rendered due to their size.
• translate_list 0 x p h_n_2 h = []

theorem translate_list_zero (n : ℕ) (x : List (Set r_3)) (p : List r_3) (h_n : n = List.length x) (h : List.length x = List.length p) (h0 : ∀ y ∈ p, y = ![0, 0, 0]) : translate_list n x p h_n h = x

theorem translate_list_length_cons (n : ℕ) (x : List (Set r_3)) (p : List r_3) (h_n : n = List.length x) (h : List.length x = List.length p) : List.length (translate_list n x p h_n h) = n

def equidecomposable (X : Set r_3) (Y : Set r_3) : Prop

Equations

• One or more equations did not get rendered due to their size.

theorem equidecomposable_self (X : Set r_3) : equidecomposable X X

instance union_isAssoc {α : Type} : Std.Associative fun (x x_1 : Set α) => union x x_1

Equations

• ⋯ = ⋯

theorem foldl_union {α : Type} (L : List (Set α)) (X : Set α) : List.foldl union X L = List.foldl union ∅ L ∪ X

theorem list_intersection_list {α : Type} (X : Set α) (a : List (Set α)) (h1 : list_intersection a = ∅) (h2 : list_union a ∩ X = ∅) : list_intersection (X :: a) = ∅

theorem equidecomposable_subset (X : Set r_3) (Y : Set r_3) (X₁ : Set r_3) (X₂ : Set r_3) (Y₁ : Set r_3) (Y₂ : Set r_3) (hx_union : X₁ ∪ X₂ = X) (hx_intersection : X₁ ∩ X₂ = ∅) (hy_union : Y₁ ∪ Y₂ = Y) (hxy_eq : X₁ = Y₁) (h_equi : equidecomposable X₂ Y₂) : equidecomposable X Y