English
For a fixed index i outside a finite set s, the family of sets obtained by mapping over the i-th coordinate of each piAntidiag fiber is pairwise disjoint.
Русский
Для фиксированного i, не принадлежащего множеству s, семейство множеств, получаемых отображением по i-координате каждого волокна piAntidiag, попарно непересекается.
LaTeX
$$$\\bigl(\\operatorname{antidiagonal} n\\bigr) \\;\\text{PairwiseDisjoint}\\;\\lambda p. \\operatorname{map}(\\text{addRightEmbedding}(\\lambda j. \\text{if } j=i \\text{ then } p.1 \\text{ else } 0))\\bigl( s.\\piAntidiag(p.2) \\bigr)$$$
Lean4
theorem pairwiseDisjoint_piAntidiag_map_addRightEmbedding (hi : i ∉ s) (n : μ) :
(antidiagonal n : Set (μ × μ)).PairwiseDisjoint fun p ↦
map (addRightEmbedding fun j ↦ if j = i then p.1 else 0) (s.piAntidiag p.2) :=
by
rintro ⟨a, b⟩ hab ⟨c, d⟩ hcd
simp only [ne_eq, antidiagonal_congr' hab hcd, disjoint_left, mem_map, mem_piAntidiag, addRightEmbedding_apply,
not_exists, not_and, and_imp, forall_exists_index]
rintro hfg _ f rfl - rfl g rfl - hgf
exact hfg <| by simpa [sum_add_distrib, hi] using congr_arg (∑ j ∈ s, · j) hgf.symm
