antidiagonalTuple_one

Mathlib.Data.Fin.Tuple.NatAntidiagonal

URI: https://scilib.ai/kg/mathlib#Finset.Nat.antidiagonalTuple_one

English

For k = 1, antidiagonalTuple 1 n equals the singleton containing the 1-tuple [n].

Русский

Для k = 1 антидиагональная кортеж суммой n равен единичному кортежу [n].

LaTeX

$$$ \operatorname{antidiagonalTuple}_{\mathrm{Finset}}(1,n) = \{ \langle n \rangle \}. $$$

Lean4

@[simp]
theorem antidiagonalTuple_one (n : ℕ) : antidiagonalTuple 1 n = {![n]} :=
  Finset.eq_of_veq (Multiset.Nat.antidiagonalTuple_one n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru