BlockSplit

noncomputable def Nibble.AX1.enumIdx {V : Type} (S : Finset V) (x : ↥S) : ℕ

The index of x ∈ S under the canonical enumeration of S.

Equations

• Nibble.AX1.enumIdx S x = ↑(S.equivFin x)

theorem Nibble.AX1.enumIdx_lt {V : Type} (S : Finset V) (x : ↥S) : enumIdx S x < S.card

theorem Nibble.AX1.enumIdx_injective {V : Type} (S : Finset V) : Function.Injective (enumIdx S)

noncomputable def Nibble.AX1.blockOf {V : Type} [DecidableEq V] (S : Finset V) (a i : ℕ) : Finset V

The i-th block of S at block size a.

Equations

• Nibble.AX1.blockOf S a i = Finset.image Subtype.val ({x ∈ S.attach | Nibble.AX1.enumIdx S x / a = i})

theorem Nibble.AX1.mem_blockOf {V : Type} [DecidableEq V] {S : Finset V} {a i : ℕ} {v : V} : v ∈ blockOf S a i ↔ ∃ (h : v ∈ S), enumIdx S ⟨v, h⟩ / a = i

theorem Nibble.AX1.blockOf_subset {V : Type} [DecidableEq V] (S : Finset V) (a i : ℕ) : blockOf S a i ⊆ S

theorem Nibble.AX1.blockOf_disjoint {V : Type} [DecidableEq V] (S : Finset V) (a : ℕ) {i j : ℕ} (hij : i ≠ j) : Disjoint (blockOf S a i) (blockOf S a j)

Distinct blocks are disjoint.

theorem Nibble.AX1.filter_div_eq_range {N a i : ℕ} (ha : 0 < a) : {j ∈ Finset.range N | j / a = i} = Finset.Ico (i * a) (min N ((i + 1) * a))

The indices lying in the i-th block form the interval [i·a, (i+1)·a).

theorem Nibble.AX1.card_blockOf {V : Type} [DecidableEq V] (S : Finset V) {a i : ℕ} (ha : 0 < a) (hfit : (i + 1) * a ≤ S.card) : (blockOf S a i).card = a

A block has exactly a elements, provided the whole of the interval [i·a, (i+1)·a) fits inside the index range of S.