English
The piAntidiag of a cons-extended set decomposes as a disjoint union of the original antidiagonal plus a mapped subfamily, with a precise disjointness condition ensuring a unique decomposition.
Русский
piAntidiag для расширенного множества через конкатенацию разлагается на дизъюнкты антидиагонали и соответствующего отображенного подмножества с явным свойством взаимной непересечаемости.
LaTeX
$$$\\pi\\mathrm{Antidiag}(\\mathrm{cons}\\ i\\ s\\ hi, n) = (\\operatorname{antidiagonal} n).\\mathrm{disjiUnion}\\Bigl(\\lambda p. \\piAntidiag(s, p.2).\\mathrm{map}(\\text{addRightEmbedding}(\\lambda t. \\text{if } t=i \\text{ then } p.fst \\text{ else } 0))\\Bigr)\\bigl( \\operatorname{pairwiseDisjoint\\ } \\piAntidiag\\_map\\_addRightEmbedding(hi, _) \\bigr)$$$
Lean4
theorem piAntidiag_cons (hi : i ∉ s) (n : μ) :
piAntidiag (cons i s hi) n =
(antidiagonal n).disjiUnion
(fun p : μ × μ ↦ (piAntidiag s p.snd).map (addRightEmbedding fun t ↦ if t = i then p.fst else 0))
(pairwiseDisjoint_piAntidiag_map_addRightEmbedding hi _) :=
by
ext f
simp only [mem_piAntidiag, sum_cons, ne_eq, mem_cons, mem_disjiUnion, mem_antidiagonal, mem_map, Prod.exists]
constructor
· rintro ⟨hn, hf⟩
refine ⟨_, _, hn, update f i 0, ⟨sum_update_of_notMem hi _ _, fun j ↦ ?_⟩, by aesop⟩
have := fun h₁ h₂ ↦ (hf j h₁).resolve_left h₂
aesop (add simp [update])
· rintro ⟨a, _, hn, g, ⟨rfl, hg⟩, rfl⟩
have := hg i
aesop (add simp [sum_add_distrib])
