English
Let C be a property on integers. If C(bit b m) holds for all b ∈ {0,1} and m ∈ ℤ, then C(n) holds for every n ∈ ℤ; i.e., any function on ℤ is determined by its values on bit representations.
Русский
Пусть C — признак на целые числа. Если C(bit b m) истинно для всех b ∈ {0,1} и m ∈ ℤ, то C(n) истинно для любого n ∈ ℤ; то есть любое свойство на ℤ задаётся значениями на битовых представлениях.
LaTeX
$$$$ \forall C:\mathbb{Z}\to \text{Sort},\ \forall n\in\mathbb{Z},\ (\forall b\in\{0,1\},\ \forall m\in\mathbb{Z},\ C(\operatorname{bit} b m)) \Rightarrow C(n). $$$$
Lean4
/-- Defines a function from `ℤ` conditionally, if it is defined for odd and even integers separately
using `bit`. -/
def bitCasesOn.{u} {C : ℤ → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n :=
by
rw [← bit_decomp n]
apply h
