piAntidiag_empty_of_ne_zero — Mathlib

English

If the index set is empty and the target sum n is nonzero, there are no functions (or tuples) assigning nonnegative values to the indices that sum to n; hence the piAntidiag set is empty whenever n ≠ 0.

Русский

Если множество индексов пусто и целевая сумма n не равна нулю, то не существует таких функций (или кортежей), которым можно было бы задать ненулевые неотрицательные значения по индексам так, чтобы их сумма дала n; поэтому piAntidiag пусто при n ≠ 0.

LaTeX

$$$\\;n \\\\neq 0 \\implies \\pi\\mathrm{Antidiag}(\\emptyset, n) = \\emptyset$$$

Lean4

@[simp]
theorem piAntidiag_empty_of_ne_zero (hn : n ≠ 0) : piAntidiag (∅ : Finset ι) n = ∅ :=
  eq_empty_of_forall_notMem (by simp [hn.symm])

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