card_antidiagonal

Mathlib.Data.Finset.NatAntidiagonal

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

← MathLib Explorer

English

The cardinality of the antidiagonal of n is n+1.

Русский

Кардинал antidiagonal(n) равен n+1.

LaTeX

$$$|\operatorname{antidiagonal}(n)| = n+1$$$

Lean4

/-- The cardinality of the antidiagonal of `n` is `n + 1`. -/
@[simp]
theorem card_antidiagonal (n : ℕ) : (antidiagonal n).card = n + 1 := by simp [antidiagonal]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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