English
For any elements n and m in the ordered additive setting, the set of pairs in the antidiagonal of n whose second coordinate equals m is empty if m > n, and is the singleton (n−m, m) if m ≤ n.
Русский
Для любых элементов n и m в упорядоченном дополняемом моноиде, множество пар в антидиагонали n с вторым компонентом, равным m, пусто при m > n, и состоит из единственного элемента (n−m, m) при m ≤ n.
LaTeX
$$$\\displaystyle \\{(k,l) \\in A\\times A \\mid k+l=n\\ \\text{and}\\ l=m\\} = \\begin{cases} \\{(n-m,m)\\}, & m \\le n, \\\\ ∅, & m>n. \\end{cases}$$$
Lean4
theorem filter_snd_eq_antidiagonal (n m : A) [DecidablePred (· = m)] [Decidable (m ≤ n)] :
{x ∈ antidiagonal n | x.snd = m} = if m ≤ n then {(n - m, m)} else ∅ :=
by
have : (fun x : A × A ↦ (x.snd = m)) ∘ Prod.swap = fun x : A × A ↦ x.fst = m := by ext; simp
rw [← map_swap_antidiagonal, filter_map]
simp [this, filter_fst_eq_antidiagonal, apply_ite (Finset.map _)]
