English
Inserting a new index i into s yields a refined decomposition of piAntidiag(·, n) as a biunion of the old piAntidiag and a transformed copy where the new coordinate is added to existing ones.
Русский
Добавление индекса i в множество s разлагает piAntidiag(·, n) на би-объединение старой piAntidiag и трансформированной копии, где новая координата добавляется к существующим.
LaTeX
$$$\\pi\\mathrm{Antidiag}(\\mathrm{insert}\\ i\\ s, n) = (\\operatorname{antidiagonal} n).\\mathrm{biUnion}\\Bigl( p : \\mu \\times \\mu \\mapsto \\pi\\mathrm{Antidiag}(s, p.2).\\mathrm{image}(\\lambda f j. f(j) + \\mathbf{1}_{j=i} \\cdot p.1)\\Bigr)$$$
Lean4
theorem piAntidiag_insert [DecidableEq (ι → μ)] (hi : i ∉ s) (n : μ) :
piAntidiag (insert i s) n =
(antidiagonal n).biUnion fun p : μ × μ ↦
(piAntidiag s p.snd).image (fun f j ↦ f j + if j = i then p.fst else 0) :=
by simpa [map_eq_image, addRightEmbedding] using piAntidiag_cons hi n
