antidiagonalTuple_two — Mathlib

English

The 2-tuple antidiagonalTuple 2 n equals the map of the ordinary diagonal n to the 2-tuple form.

Русский

2-мерная антидиагональ задаётся отображением пары (i,j) с i+j=n на форму ![i,j].

LaTeX

$$$ antidiagonalTuple 2 n = (antidiagonal n).map (fun i => ![i.1, i.2]) $$$

Lean4

theorem antidiagonalTuple_two (n : ℕ) : antidiagonalTuple 2 n = (antidiagonal n).map fun i => ![i.1, i.2] :=
  by
  rw [antidiagonalTuple]
  simp_rw [antidiagonalTuple_one, List.map_singleton]
  rw [List.map_eq_flatMap]
  rfl

Похожие утверждения