instHasAntidiagonal — Mathlib

English

For every natural number n, the antidiagonal consists of all pairs of natural numbers (i,j) with i+j = n.

Русский

Для каждого натурального числа n антидиагональ состоит из всех пар (i,j) целых чисел, удовлетворяющих i+j = n.

LaTeX

$$$\operatorname{antidiagonal}(n) = \{(i,j) \in \mathbb{N}^2 : i+j=n\}$$$

Lean4

/-- The antidiagonal of a natural number `n` is
    the finset of pairs `(i, j)` such that `i + j = n`. -/
instance instHasAntidiagonal : HasAntidiagonal ℕ
    where
  antidiagonal n := ⟨Multiset.Nat.antidiagonal n, Multiset.Nat.nodup_antidiagonal n⟩
  mem_antidiagonal {n} {xy} := by rw [mem_def, Multiset.Nat.mem_antidiagonal]

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