English
Characterisation: an f lies in piAntidiag s n exactly when the sum over i of f(i) equals n and all nonzero entries lie in s.
Русский
Характеризация: функция f принадлежит piAntidiag s n тогда, когда сумма f(i) по i равна n и все ненулевые значения лежат в s.
LaTeX
$$$f\in\text{piAntidiag}(s,n) \iff \sum_i f(i) = n \land \forall i, f(i) \neq 0 \Rightarrow i\in s$$$
Lean4
/-- The finset of functions `ι → μ` with support contained in `s` and sum `n`. -/
def piAntidiag (s : Finset ι) (n : μ) : Finset (ι → μ) :=
by
refine
(Fintype.truncEquivFinOfCardEq <| Fintype.card_coe s).lift
(fun e ↦ (finAntidiagonal s.card n).map ⟨fun f i ↦ if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, ?_⟩) fun e₁ e₂ ↦ ?_
· rintro f g hfg
ext i
simpa using congr_fun hfg (e.symm i)
· ext f
simp only [mem_map, mem_finAntidiagonal]
refine Equiv.exists_congr ((e₁.symm.trans e₂).arrowCongr <| .refl _) fun g ↦ ?_
have := Fintype.sum_equiv (e₂.symm.trans e₁) _ g fun _ ↦ rfl
simp_all
