Basic lemmas on flipSet, antipode, diffSet, zone

theorem AaronsonAmbainis.flipSet_apply {ι : Type u_1} [DecidableEq ι] (x : Cube ι) (S : Finset ι) (i : ι) : flipSet x S i = if i ∈ S then !x i else x i

theorem AaronsonAmbainis.mem_diffSet {ι : Type u_1} [Fintype ι] {x y : Cube ι} {i : ι} : i ∈ diffSet x y ↔ x i ≠ y i

theorem AaronsonAmbainis.mem_zone {ι : Type u_1} [Fintype ι] [DecidableEq ι] {g : Cube ι → Bool} {u : Cube ι} : u ∈ zone g ↔ g u = true ∧ g (antipode u) = false

theorem AaronsonAmbainis.card_cube {ι : Type u_1} [Fintype ι] [DecidableEq ι] : Fintype.card (Cube ι) = 2 ^ Fintype.card ι