English
In a canonically ordered additive monoid, the antidiagonal is constructed by filtering the square Iic(n) × Iic(n) to those pairs whose sum is n. In other words, antidiagonal(n) = { (a,b) ∈ Iic(n) × Iic(n) | a+b = n }.
Русский
В канонически упорядоченном аддитивном монойде антидиагональ строится отборами внутри квадрата Iic(n) × Iic(n) пар, чьи суммы равны n; то есть antidiagonal(n) = { (a,b) ∈ Iic(n) × Iic(n) | a+b = n }.
LaTeX
$$$ antidiagonal(n) = \\{(a,b) ∈ Iic(n) \\times Iic(n) \\mid a+b = n\\}.$$$
Lean4
/-- In a canonically ordered additive monoid, the antidiagonal can be construct by filtering.
Note that this is not an instance, as for some times a more efficient algorithm is available. -/
abbrev antidiagonalOfLocallyFinite : HasAntidiagonal A
where
antidiagonal n := {uv ∈ Iic n ×ˢ Iic n | uv.fst + uv.snd = n}
mem_antidiagonal {n}
{a} := by
simp only [mem_filter, and_iff_right_iff_imp]
intro h
simp [← h]
