mathlib3 documentation

data.finset.nat_antidiagonal

Antidiagonals in ℕ × ℕ as finsets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the antidiagonals of ℕ × ℕ as finsets: the n-th antidiagonal is the finset of pairs (i, j) such that i + j = n. This is useful for polynomial multiplication and more generally for sums going from 0 to n.

Notes #

This refines files data.list.nat_antidiagonal and data.multiset.nat_antidiagonal.

source
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
source
@[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.

source
@[simp]
theorem finset.nat.card_antidiagonal (n : ℕ) :
(finset.nat.antidiagonal n).card = n + 1

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

source
@[simp]
theorem finset.nat.antidiagonal_zero  :
finset.nat.antidiagonal 0 = {(0, 0)}

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

source
theorem finset.nat.antidiagonal_succ (n : ℕ) :
finset.nat.antidiagonal (n + 1) = finset.cons (0, n + 1) (finset.map ({to_fun := nat.succ, inj' := nat.succ_injective}.prod_map (function.embedding.refl ℕ)) (finset.nat.antidiagonal n)) _
source
theorem finset.nat.antidiagonal_succ' (n : ℕ) :
finset.nat.antidiagonal (n + 1) = finset.cons (n + 1, 0) (finset.map ((function.embedding.refl ℕ).prod_map {to_fun := nat.succ, inj' := nat.succ_injective}) (finset.nat.antidiagonal n)) _
source
theorem finset.nat.antidiagonal_succ_succ' {n : ℕ} :
finset.nat.antidiagonal (n + 2) = finset.cons (0, n + 2) (finset.cons (n + 2, 0) (finset.map ({to_fun := nat.succ, inj' := nat.succ_injective}.prod_map {to_fun := nat.succ, inj' := nat.succ_injective}) (finset.nat.antidiagonal n)) _) _
source
theorem finset.nat.map_swap_antidiagonal {n : ℕ} :
finset.map {to_fun := prod.swap ℕ, inj' := _} (finset.nat.antidiagonal n) = finset.nat.antidiagonal n
source
theorem finset.nat.antidiagonal_congr {n : ℕ} {p q : ℕ × ℕ} (hp : p ∈ finset.nat.antidiagonal n) (hq : q ∈ finset.nat.antidiagonal n) :
p = q ↔ p.fst = q.fst

A point in the antidiagonal is determined by its first co-ordinate.

source
theorem finset.nat.antidiagonal.fst_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ finset.nat.antidiagonal n) :
kl.fst ≤ n
source
theorem finset.nat.antidiagonal.snd_le {n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ finset.nat.antidiagonal n) :
kl.snd ≤ n
source
theorem finset.nat.filter_fst_eq_antidiagonal (n m : ℕ) :
finset.filter (λ (x : ℕ × ℕ), x.fst = m) (finset.nat.antidiagonal n) = ite (m ≤ n) {(m, n - m)} ∅
source
theorem finset.nat.filter_snd_eq_antidiagonal (n m : ℕ) :
finset.filter (λ (x : ℕ × ℕ), x.snd = m) (finset.nat.antidiagonal n) = ite (m ≤ n) {(n - m, m)} ∅
source
def finset.nat.sigma_antidiagonal_equiv_prod  :
(Σ (n : ℕ), ↥(finset.nat.antidiagonal n)) ≃ ℕ × ℕ

The disjoint union of antidiagonals Σ (n : ℕ), antidiagonal n is equivalent to the product ℕ × ℕ. This is such an equivalence, obtained by mapping (n, (k, l)) to (k, l).

Equations
source
@[simp]
theorem finset.nat.sigma_antidiagonal_equiv_prod_apply (x : Σ (n : ℕ), ↥(finset.nat.antidiagonal n)) :
⇑finset.nat.sigma_antidiagonal_equiv_prod x = ↑(x.snd)
source
@[simp]
theorem finset.nat.sigma_antidiagonal_equiv_prod_symm_apply_snd_coe (x : ℕ × ℕ) :
↑((⇑(finset.nat.sigma_antidiagonal_equiv_prod.symm) x).snd) = x
source
@[simp]
theorem finset.nat.sigma_antidiagonal_equiv_prod_symm_apply_fst (x : ℕ × ℕ) :
(⇑(finset.nat.sigma_antidiagonal_equiv_prod.symm) x).fst = x.fst + x.snd