antidiagonalTuple_zero_zero — Mathlib

English

There is a unique 0-tuple of natural numbers whose sum is 0; the 0-sum tuple is the empty function.

Русский

Существует единственный 0-сложный кортеж из неотрицательных целых чисел, сумма которого равна 0; это пустой 0-upleт.

LaTeX

$$$ \operatorname{antidiagonalTuple}(0,0) = \{ f : \mathrm{Fin}(0) \to \mathbb{N} \mid \mathrm{True} \}. $$$

Lean4

@[simp]
theorem antidiagonalTuple_zero_zero : antidiagonalTuple 0 0 = {![]} :=
  rfl

Похожие утверждения