English
There is a natural bijection between triples (k,l,S) with S a Finset of Fin(k+l) of size l and pairs (n,S) with S a Finset of Fin n, given by forward map (k,l,S) ↦ (k+l,S) and inverse map (n,S) ↦ (n−|S|, |S|, S).
Русский
Существует естественная биекция между тройками (k,l,S) с S — конечный набор элементов Fin(k+l) размера l и парами (n,S) с S ⊆ Fin n: отображение (k,l,S) ↦ (k+l,S) и обратное (n,S) ↦ (n−|S|, |S|, S).
LaTeX
$$$\\text{changeOriginIndexEquiv}: (\\Sigma k,l,\\{ s: Finset(Fin(k+l)) \\mid s.card = l \\}) \\simeq \\Sigma n, Finset(Fin n)$$$
Lean4
/-- Changing the origin of a formal multilinear series `p`, so that
`p.sum (x+y) = (p.changeOrigin x).sum y` when this makes sense.
-/
def changeOrigin (x : E) : FormalMultilinearSeries 𝕜 E F := fun k => (p.changeOriginSeries k).sum x
