English
The antidiagonal operation is defined for Finset of Finsupp α ℕ as a finset of pairs whose sum is the given function.
Русский
Операция антидиагонали определяется для Finset в Finsupp α ℕ как множество пар, сумма которых равна заданной функции.
LaTeX
$$instance\\ instHasAntidiagonal : HasAntidiagonal (α →₀ ℕ) where\\ antidiagonal f := f.antidiagonal'.support$$
Lean4
/-- The antidiagonal of `s : α →₀ ℕ` is the finset of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)`
such that `t₁ + t₂ = s`. -/
instance instHasAntidiagonal : HasAntidiagonal (α →₀ ℕ)
where
antidiagonal f := f.antidiagonal'.support
mem_antidiagonal {f}
{p} := by
rcases p with ⟨p₁, p₂⟩
simp [antidiagonal', ← and_assoc, Multiset.toFinsupp_eq_iff, ← Multiset.toFinsupp_eq_iff (f := f)]
