fst_lt

Mathlib.Data.Finset.NatAntidiagonal

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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