antidiagonalTuple_two — Mathlib

English

The 2-tuple antidiagonal is the set of all functions f : Fin 2 → ℕ with f(0) + f(1) = n.

Русский

Антидиагональ для 2‑кортежей состоит из всех функций f: Fin 2 → ℕ такие, что f(0) + f(1) = n.

LaTeX

$$$ \operatorname{antidiagonalTuple}_{\mathrm{Finset}}(2,n) = \{ f : \mathrm{Fin}(2) \to \mathbb{N} \mid f(0) + f(1) = n \}. $$$

Lean4

theorem antidiagonalTuple_two (n : ℕ) :
    antidiagonalTuple 2 n = (antidiagonal n).map (piFinTwoEquiv fun _ => ℕ).symm.toEmbedding :=
  Finset.eq_of_veq (Multiset.Nat.antidiagonalTuple_two n)

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