antidiagonalTuple_zero_right — Mathlib

English

For any k, antidiagonalTuple k 0 equals the singleton {0}, i.e., the zero k-tuple.

Русский

Для любого k antidiagonalTuple k 0 равно единичному множеству {0}, то есть нулевой k‑кортеж.

LaTeX

$$$ \operatorname{antidiagonalTuple}_{\mathrm{Finset}}(k,0) = \{ \mathbf{0}_k \}. $$$

Lean4

theorem antidiagonalTuple_zero_right (k : ℕ) : antidiagonalTuple k 0 = {0} :=
  Finset.eq_of_veq (Multiset.Nat.antidiagonalTuple_zero_right k)

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