English
Nimber multiplication is defined by the given formula: a*b equals the infimum of the complement of the set of x for which there exist a'<a, b'<b with a'*b + a*b' + a'*b' = x.
Русский
Умножение Nimber задаётся формулой: a*b равняется инфимума дополнения множества {x | существует a'<a, существует b'<b, a'*b + a*b' + a'*b' = x}.
LaTeX
$$$ a \cdot b = \operatorname{sInf} \{ x \mid \exists a' < a, \exists b' < b, a' \cdot b + a \cdot b' + a' \cdot b' = x \}^{\complement}$$$
Lean4
theorem mul_def (a b : Nimber) : a * b = sInf {x | ∃ a' < a, ∃ b' < b, a' * b + a * b' + a' * b' = x}ᶜ :=
by
change Nimber.mul a b = _
rw [Nimber.mul]
simp_rw [exists_prop]
rfl
