mem_finAntidiagonal — Mathlib

English

A function f belongs to finAntidiagonal d n if and only if the sum of its coordinates equals n.

Русский

Функция f принадлежит finAntidiagonal d n тогда и только тогда, когда сумма её координат равна n.

LaTeX

$$$f\in\text{finAntidiagonal}(d,n) \iff \sum_i f(i) = n$$$

Lean4

@[simp]
theorem mem_finAntidiagonal {d : ℕ} {f : Fin d → μ} : f ∈ finAntidiagonal d n ↔ ∑ i, f i = n :=
  (finAntidiagonal.aux d n).prop f

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