antidiagonal_zero

Mathlib.Data.Finsupp.Antidiagonal

URI: https://scilib.ai/kg/mathlib#Finsupp.antidiagonal_zero

English

The antidiagonal of the zero function is the singleton containing (0,0).

Русский

Антидиагональ нулевой функции равна одиночному множеству, содержащему (0,0).

LaTeX

$$$\\operatorname{antidiagonal}(0) = \\{(0,0)\\}$$$

Lean4

@[simp]
theorem antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = singleton (0, 0) :=
  rfl

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

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

Разделы

Аффилиация

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