mem_antidiagonalTuple — Mathlib

English

For any n, k and x : Fin k → ℕ, x is in antidiagonalTuple k n iff the sum of its coordinates equals n.

Русский

Пусть x : Fin k → ℕ; тогда x ∈ antidiagonalTuple k n тогда и только тогда, когда сумма координат x равна n.

LaTeX

$$$ {n : \mathbb{N}} {k : \mathbb{N}} {x : \mathrm{Fin}(k) \to \mathbb{N}} : x \in \operatorname{antidiagonalTuple}(k,n) \iff \sum_{i : \mathrm{Fin}(k)} x(i) = n. $$$

Lean4

theorem mem_antidiagonalTuple {n : ℕ} {k : ℕ} {x : Fin k → ℕ} : x ∈ antidiagonalTuple k n ↔ ∑ i, x i = n :=
  List.Nat.mem_antidiagonalTuple

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