antidiagonal_eq_map' — Mathlib

English

Equivalently, antidiagonal n is the image of range(n+1) under i ↦ (n−i,i).

Русский

Эквивалентно, антидиагональ n есть образ range(n+1) при отображении i↦(n−i,i).

LaTeX

$$$\operatorname{antidiagonal}(n) = \operatorname{range}(n+1) \mapsto (n-i,i)$$$

Lean4

theorem antidiagonal_eq_map' (n : ℕ) :
    antidiagonal n = (range (n + 1)).map ⟨fun i ↦ (n - i, i), fun _ _ h ↦ (Prod.ext_iff.1 h).2⟩ := by
  rw [← map_swap_antidiagonal, antidiagonal_eq_map, map_map]; rfl

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