English
The piAntidiag structure on the universal finite set corresponds, via a natural boolean-arrow equivalence, to the standard antidiagonal relation; there is a canonical bijection identifying these two representations.
Русский
Структура piAntidiag на универсальном конечном множестве идентифицируется с обычной антидиагональю через естественное эквиволиентство, образуя каноническое соответствие между двумя представлениями.
LaTeX
$$$\\operatorname{Equiv.finsetCongr}(\\operatorname{Equiv.boolArrowEquivProd}_{\\mu})\\bigl(\\piAntidiag(\\mathrm{univ}, n)\\bigr) = \\operatorname{antidiagonal}(n)$$$
Lean4
theorem finsetCongr_piAntidiag_eq_antidiag (n : μ) :
Equiv.finsetCongr (Equiv.boolArrowEquivProd _) (piAntidiag univ n) = antidiagonal n :=
by
ext ⟨x₁, x₂⟩
simp_rw [Equiv.finsetCongr_apply, mem_map, Equiv.toEmbedding, Function.Embedding.coeFn_mk, ← Equiv.eq_symm_apply]
simp [add_comm]
