English
Let n be a natural number. The antidiagonal of n is the list of pairs (i, n − i) for i = 0,1,...,n. If we swap the components of each pair and then reverse the resulting list, we get exactly the same list as just reversing the original antidiagonal.
Русский
Пусть n ∈ ℕ. Антидиагональ n задаётся как упорядоченный список пар (i, n − i), где i = 0,1,…,n. Замена компонент в каждой паре и последующее развёртывание списка дают тот же результат, что и просто развёрнутая исходная антидиагональ.
LaTeX
$$$ (\operatorname{antidiagonal}(n)).\operatorname{map}(\mathrm{Prod.swap}) = (\operatorname{antidiagonal}(n)).\operatorname{reverse} $$$
Lean4
theorem map_swap_antidiagonal {n : ℕ} : (antidiagonal n).map Prod.swap = (antidiagonal n).reverse :=
by
rw [antidiagonal, map_map, ← List.map_reverse, range_eq_range', reverse_range', ← range_eq_range', map_map]
apply map_congr_left
simp +contextual [Nat.sub_sub_self, Nat.lt_succ_iff]
