snd_lt

Mathlib.Data.Finset.NatAntidiagonal

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

English

If (i,j) ∈ antidiagonal(n), then j < n+1.

Русский

Если (i,j) ∈ антидиагональ(n), то j < n+1.

LaTeX

$$snd bound: $(i,j) \\in \\operatorname{antidiagonal}(n) \\Rightarrow j < n+1$$$

Lean4

theorem snd_lt {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.2 < n + 1 :=
  Nat.lt_succ_of_le <| antidiagonal.snd_le hlk

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

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

Разделы

Аффилиация

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