mem_antidiagonal — Mathlib

English

An ordered pair x is in the antidiagonal of n if and only if its components sum to n.

Русский

Пара x перейдет к антидиагонали n тогда и только тогда, когда суммы её координат равны n.

LaTeX

$$$x \\in \\mathrm{antidiagonal}(n) \\iff x_1 + x_2 = n$.$$

Lean4

/-- A pair (i, j) is contained in the antidiagonal of `n` if and only if `i + j = n`. -/
@[simp]
theorem mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} : x ∈ antidiagonal n ↔ x.1 + x.2 = n := by
  rw [antidiagonal, mem_coe, List.Nat.mem_antidiagonal]

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