antidiagonal_eq_image — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem antidiagonal_eq_image (n : ℕ) : antidiagonal n = (range (n + 1)).image fun i ↦ (i, n - i) := by
  simp only [antidiagonal_eq_map, map_eq_image, Function.Embedding.coeFn_mk]

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