def same_orbit (a : r_3) (b : r_3) : Prop

Equations

• same_orbit a b = ∃ (p : ↥G), rotate (↑p) a = b

def orbit_A (a : r_3) : Set ↑L

Equations

• orbit_A a = {b : ↑L | same_orbit a ↑b}

def list_intersection_pairwise (α : Type) (w : List (Set α)) : Prop

Equations

• list_intersection_pairwise α w = ∀ (i j : Fin (List.length w)), i ≠ j → List.get w i ∩ List.get w j = ∅

def all_orbits : Set (Set r_3)

Equations

• all_orbits = {w : Set r_3 | ∃ (x : ↑L), Set.Nonempty w ∧ Subtype.val '' orbit_A ↑x = w}

theorem all_orbits_countable : Set.Countable all_orbits

noncomputable def choose (x : Set r_3) (hx : x ∈ all_orbits) : r_3

Equations

• choose x hx = Id.run (let_fun h := ⋯; pure (Classical.choose h))

def M : Set r_3

Equations

• M = {w : r_3 | ∃ (x : Set r_3) (hx : x ∈ all_orbits), choose x hx = w}

theorem M_countable : Set.Countable M