snd_le

Mathlib.Algebra.Order.Antidiag.Prod

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

← MathLib Explorer

English

Similarly, the second coordinate of any pair in the antidiagonal is at most n.

Русский

Аналогично, вторая координата пары в антидиагонали не превышает n.

LaTeX

$$$\\forall k\\in\\operatorname{antidiagonal}(n), k_2 \\le n$$$

Lean4

theorem snd_le {n : A} {kl : A × A} (hlk : kl ∈ antidiagonal n) : kl.2 ≤ n :=
  by
  rw [le_iff_exists_add]
  use kl.1
  rwa [mem_antidiagonal, eq_comm, add_comm] at hlk

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

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

Разделы

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

Аффилиация

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