The finsupp counterpart of multiset.antidiagonal. #
The antidiagonal of s : α →₀ ℕ consists of
all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.
The finsupp counterpart of multiset.antidiagonal: the antidiagonal of
s : α →₀ ℕ consists of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ) such that t₁ + t₂ = s.
The finitely supported function antidiagonal s is equal to the multiplicities of these pairs.
The antidiagonal of s : α →₀ ℕ is the finset of all pairs (t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)
such that t₁ + t₂ = s.
Equations
theorem
finsupp.swap_mem_antidiagonal
{α : Type u_1}
{n : α →₀ ℕ}
{f : (α →₀ ℕ) × (α →₀ ℕ)} :
f.swap ∈ n.antidiagonal ↔ f ∈ n.antidiagonal