mathlib documentation

data.finset.nat_antidiagonal

The "antidiagonal" {(0,n), (1,n-1), ..., (n,0)} as a finset.

def finset.nat.antidiagonal (n : ℕ) :

finset (ℕ × ℕ)

The antidiagonal of a natural number n is the finset of pairs (i,j) such that i+j = n.

Equations

finset.nat.antidiagonal n = {val := multiset.nat.antidiagonal n, nodup := _}

@[simp]

theorem finset.nat.mem_antidiagonal {n : ℕ} {x : ℕ × ℕ} :

x ∈ finset.nat.antidiagonal n ↔ x.fst + x.snd = n

A pair (i,j) is contained in the antidiagonal of n if and only if i+j=n.

@[simp]

theorem finset.nat.card_antidiagonal (n : ℕ) :

(finset.nat.antidiagonal n).card = n + 1

The cardinality of the antidiagonal of n is n+1.

@[simp]

theorem finset.nat.antidiagonal_zero :

finset.nat.antidiagonal 0 = {(0, 0)}

The antidiagonal of 0 is the list [(0,0)]

theorem finset.nat.antidiagonal_succ {n : ℕ} :

finset.nat.antidiagonal (n + 1) = insert (0, n + 1) (finset.map ({to_fun := nat.succ, inj' := nat.succ_injective}.prod_map (function.embedding.refl ℕ)) (finset.nat.antidiagonal n))

theorem finset.nat.map_swap_antidiagonal {n : ℕ} :

finset.map {to_fun := prod.swap ℕ, inj' := _} (finset.nat.antidiagonal n) = finset.nat.antidiagonal n