Behrend.mem_box
theorem Behrend.mem_box : ∀ {n d : ℕ} {x : Fin n → ℕ}, x ∈ Behrend.box n d ↔ ∀ (i : Fin n), x i < d
The theorem `Behrend.mem_box` states that for any natural numbers `n` and `d`, and any function `x` from `Fin n` to `ℕ`, `x` is an element of the Behrend box of dimension `n` with side length `d` if and only if for every element `i` in `Fin n`, the value `x(i)` is less than `d`. In other words, every point in the `n`-dimensional box has coordinates strictly less than `d`.
More concisely: A function from Fin n to ℕ is an element of the Behrend box of dimension n with side length d if and only if its values are strictly less than d for all i in Fin n.
|
Behrend.map_succ
theorem Behrend.map_succ :
∀ {n d : ℕ} (a : Fin (n + 1) → ℕ), (Behrend.map d) a = a 0 + (Finset.univ.sum fun x => a x.succ * d ^ ↑x) * d := by
sorry
The theorem `Behrend.map_succ` states that for any natural numbers `n` and `d`, and a function `a` from `Fin (n + 1)` to `ℕ`, the map associated with `Behrend.map` when applied to `a` is equal to `a(0)` plus the sum, over all elements `x` in the finite set `Finset.univ`, of `a(Fin.succ(x)) * d ^ ↑x`, all multiplied by `d`. Essentially, this theorem describes how the Behrend map behaves when it is applied to a function on the successor of a finite ordinal number.
More concisely: For any natural numbers `n` and `d`, and a function `a` from `Fin (n + 1)` to `ℕ`, the Behrend map of `a` is equal to `a(0) + ∑ₕ in Finset.univ {d ^ up x * a (Fin.succ x)}`.
|