fst_le — Mathlib

English

Any pair in the antidiagonal satisfies that its first coordinate is at most the sum n.

Русский

Любая пара в антидиагонали имеет первую координату не большую чем сумма n.

LaTeX

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

Lean4

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

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