Partial HasAntidiagonal for functions with finite support #
For an AddCommMonoid
μ
,
Finset.HasAntidiagonal μ
provides a function antidiagonal : μ → Finset (μ × μ)
which maps n : μ
to a Finset
of pairs (a, b)
such that a + b = n
.
In this file, we provide an analogous definition for ι →₀ μ
,
with an explicit finiteness condition on the support,
assuming AddCommMonoid μ
, HasAntidiagonal μ
,
For computability reasons, we also need DecidableEq ι
and DecidableEq μ
.
This Finset could be viewed inside ι → μ
,
but the Finsupp
condition provides a natural DecidableEq
instance.
Main definitions #
Finset.piAntidiagonal s n
is the finite set of all functions with finite support contained ins
and sumn : μ
That condition is expressed byFinset.mem_piAntidiagonal
Finset.mem_piAntidiagonal'
rewrites theFinsupp.sum
condition as aFinset.sum
.Finset.finAntidiagonal
, a more general case ofFinset.Nat.antidiagonalTuple
(TODO: deduplicate).
finAntidiagonal d n
is the type of d
-tuples with sum n
.
TODO: deduplicate with the less general Finset.Nat.antidiagonalTuple
.
Equations
- Finset.finAntidiagonal d n = ↑(Finset.finAntidiagonal.aux d n)
Instances For
Auxiliary construction for finAntidiagonal
that bundles a proof of lawfulness
(mem_finAntidiagonal
), as this is needed to invoke disjiUnion
. Using Finset.disjiUnion
makes
this computationally much more efficient than using Finset.biUnion
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
finAntidiagonal₀ d n
is the type of d-tuples with sum n
Equations
- One or more equations did not get rendered due to their size.
Instances For
The Finset of functions ι →₀ μ
with support contained in s
and sum n
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A function belongs to piAntidiagonal s n
iff its support is contained in s
and the sum of its components is equal to n