Mathlib.Data.Finset.NatAntidiagonal

Finset.Nat.instHasAntidiagonal instance

: HasAntidiagonal ℕ

Full source

/-- The antidiagonal of a natural number `n` is
    the finset of pairs `(i, j)` such that `i + j = n`. -/
instance instHasAntidiagonal : HasAntidiagonal ℕ where
  antidiagonal n := ⟨Multiset.Nat.antidiagonal n, Multiset.Nat.nodup_antidiagonal n⟩
  mem_antidiagonal {n} {xy} := by
    rw [mem_def, Multiset.Nat.mem_antidiagonal]

The Antidiagonal of a Natural Number as a Finite Set

Informal description

For any natural number $n$, the antidiagonal of $n$ is the finite set of pairs $(i, j)$ of natural numbers such that $i + j = n$. This set consists of the pairs $(0, n), (1, n-1), \ldots, (n, 0)$.

Finset.Nat.antidiagonal_eq_map theorem

(n : ℕ) : antidiagonal n = (range (n + 1)).map ⟨fun i ↦ (i, n - i), fun _ _ h ↦ (Prod.ext_iff.1 h).1⟩

Full source

lemma antidiagonal_eq_map (n : ℕ) :
    antidiagonal n = (range (n + 1)).map ⟨fun i ↦ (i, n - i), fun _ _ h ↦ (Prod.ext_iff.1 h).1⟩ :=
  rfl

Antidiagonal as Map of Range for Natural Numbers

Informal description

For any natural number $n$, the antidiagonal set $\operatorname{antidiagonal}(n)$ is equal to the image of the range $\{0, \ldots, n\}$ under the map $i \mapsto (i, n - i)$.

Finset.Nat.antidiagonal_eq_map' theorem

(n : ℕ) : antidiagonal n = (range (n + 1)).map ⟨fun i ↦ (n - i, i), fun _ _ h ↦ (Prod.ext_iff.1 h).2⟩

Full source

lemma 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

Antidiagonal as Image of Range under Swapped Pair Map

Informal description

For any natural number $n$, the antidiagonal set $\operatorname{antidiagonal}(n) = \{(i, j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n\}$ is equal to the image of the finite set $\{0, 1, \ldots, n\}$ under the injective map $i \mapsto (n - i, i)$.

Finset.Nat.antidiagonal_eq_image theorem

(n : ℕ) : antidiagonal n = (range (n + 1)).image fun i ↦ (i, n - i)

Full source

lemma 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]

Antidiagonal as Image of Range for Natural Numbers

Informal description

For any natural number $n$, the antidiagonal set $\{(i, j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n\}$ is equal to the image of the function $i \mapsto (i, n - i)$ applied to the finite set $\{0, 1, \ldots, n\}$.

Finset.Nat.antidiagonal_eq_image' theorem

(n : ℕ) : antidiagonal n = (range (n + 1)).image fun i ↦ (n - i, i)

Full source

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

Antidiagonal as Image of Range under Reversed Pair Mapping

Informal description

For any natural number $n$, the antidiagonal set $\{(i, j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n\}$ is equal to the image of the finite set $\{0, 1, \ldots, n\}$ under the mapping $i \mapsto (n - i, i)$.

Finset.Nat.card_antidiagonal theorem

(n : ℕ) : (antidiagonal n).card = n + 1

Full source

/-- The cardinality of the antidiagonal of `n` is `n + 1`. -/
@[simp]
theorem card_antidiagonal (n : ℕ) : (antidiagonal n).card = n + 1 := by simp [antidiagonal]

Cardinality of Antidiagonal: $|\text{antidiagonal}(n)| = n + 1$

Informal description

For any natural number $n$, the cardinality of the finite set of pairs $(i, j) \in \mathbb{N} \times \mathbb{N}$ such that $i + j = n$ is $n + 1$.

Finset.Nat.antidiagonal_zero theorem

: antidiagonal 0 = {(0, 0)}

Full source

/-- The antidiagonal of `0` is the list `[(0, 0)]` -/
@[simp]
theorem antidiagonal_zero : antidiagonal 0 = {(0, 0)} := rfl

Antidiagonal of Zero is Singleton $\{(0, 0)\}$

Informal description

The antidiagonal of the natural number $0$ is the finite set $\{(0, 0)\}$.

Finset.Nat.antidiagonal_succ theorem

 (n : ℕ) :
  antidiagonal (n + 1) =
    cons (0, n + 1) ((antidiagonal n).map (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ (Embedding.refl _)))
      (by simp)

Full source

theorem antidiagonal_succ (n : ℕ) :
    antidiagonal (n + 1) =
      cons (0, n + 1)
        ((antidiagonal n).map
          (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ (Embedding.refl _)))
        (by simp) := by
  apply eq_of_veq
  rw [cons_val, map_val]
  apply Multiset.Nat.antidiagonal_succ

Recursive Construction of the Antidiagonal Set: $\text{antidiagonal}(n+1) = \{(0, n+1)\} \cup \{(i+1, j) \mid (i, j) \in \text{antidiagonal}(n)\}$

Informal description

For any natural number $n$, the antidiagonal set of $n+1$ is given by: \[ \text{antidiagonal}(n+1) = \{(0, n+1)\} \cup \{(i+1, j) \mid (i, j) \in \text{antidiagonal}(n)\} \] where $\text{antidiagonal}(n)$ denotes the finite set of pairs $(i, j)$ of natural numbers such that $i + j = n$.

Finset.Nat.antidiagonal_succ' theorem

 (n : ℕ) :
  antidiagonal (n + 1) =
    cons (n + 1, 0) ((antidiagonal n).map (Embedding.prodMap (Embedding.refl _) ⟨Nat.succ, Nat.succ_injective⟩))
      (by simp)

Full source

theorem antidiagonal_succ' (n : ℕ) :
    antidiagonal (n + 1) =
      cons (n + 1, 0)
        ((antidiagonal n).map
          (Embedding.prodMap (Embedding.refl _) ⟨Nat.succ, Nat.succ_injective⟩))
        (by simp) := by
  apply eq_of_veq
  rw [cons_val, map_val]
  exact Multiset.Nat.antidiagonal_succ'

Recursive Construction of Antidiagonal Set via Left Successor: $\text{antidiagonal}(n+1) = \{(n+1, 0)\} \cup \{(i, j+1)\}_{(i,j) \in \text{antidiagonal}(n)}$

Informal description

For any natural number $n$, the antidiagonal set of $n+1$ is given by: \[ \text{antidiagonal}(n+1) = \{(n+1, 0)\} \cup \{(i, j+1) \mid (i, j) \in \text{antidiagonal}(n)\} \] where $\text{antidiagonal}(n)$ denotes the finite set of pairs $(i, j)$ of natural numbers such that $i + j = n$.

Finset.Nat.antidiagonal_succ_succ' theorem

 {n : ℕ} :
  antidiagonal (n + 2) =
    cons (0, n + 2)
      (cons (n + 2, 0)
          ((antidiagonal n).map (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩ ⟨Nat.succ, Nat.succ_injective⟩)) <|
        by simp)
      (by simp)

Full source

theorem antidiagonal_succ_succ' {n : ℕ} :
    antidiagonal (n + 2) =
      cons (0, n + 2)
        (cons (n + 2, 0)
            ((antidiagonal n).map
              (Embedding.prodMap ⟨Nat.succ, Nat.succ_injective⟩
                ⟨Nat.succ, Nat.succ_injective⟩)) <|
          by simp)
        (by simp) := by
  simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', Finset.map_cons, map_map]
  rfl

Recursive Construction of Antidiagonal Set for $n+2$: $\text{antidiagonal}(n+2) = \{(0, n+2), (n+2, 0)\} \cup \{(i+1, j+1)\}_{(i,j) \in \text{antidiagonal}(n)}$

Informal description

For any natural number $n$, the antidiagonal set of $n+2$ is given by: \[ \text{antidiagonal}(n+2) = \{(0, n+2)\} \cup \{(n+2, 0)\} \cup \{(i+1, j+1) \mid (i, j) \in \text{antidiagonal}(n)\} \] where $\text{antidiagonal}(n)$ denotes the finite set of pairs $(i, j)$ of natural numbers such that $i + j = n$.

Finset.Nat.antidiagonal.fst_lt theorem

{n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.1 < n + 1

Full source

theorem antidiagonal.fst_lt {n : ℕ} {kl : ℕℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.1 < n + 1 :=
  Nat.lt_succ_of_le <| antidiagonal.fst_le hlk

First Component Bound in Antidiagonal: $k < n + 1$

Informal description

For any natural number $n$ and any pair $(k, l) \in \mathbb{N} \times \mathbb{N}$ in the antidiagonal of $n$ (i.e., $k + l = n$), the first component $k$ satisfies $k < n + 1$.

Finset.Nat.antidiagonal.snd_lt theorem

{n : ℕ} {kl : ℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.2 < n + 1

Full source

theorem antidiagonal.snd_lt {n : ℕ} {kl : ℕℕ × ℕ} (hlk : kl ∈ antidiagonal n) : kl.2 < n + 1 :=
  Nat.lt_succ_of_le <| antidiagonal.snd_le hlk

Second Component Bound in Natural Number Antidiagonal

Informal description

For any natural number $n$ and any pair $(k, l) \in \mathbb{N} \times \mathbb{N}$ in the antidiagonal of $n$ (i.e., satisfying $k + l = n$), the second component $l$ is strictly less than $n + 1$.

Finset.Nat.antidiagonal_filter_snd_le_of_le theorem

 {n k : ℕ} (h : k ≤ n) :
  {a ∈ antidiagonal n | a.snd ≤ k} =
    (antidiagonal k).map (Embedding.prodMap ⟨_, add_left_injective (n - k)⟩ (Embedding.refl ℕ))

Full source

@[simp] lemma antidiagonal_filter_snd_le_of_le {n k : ℕ} (h : k ≤ n) :
    {a ∈ antidiagonal n | a.snd ≤ k} = (antidiagonal k).map
      (Embedding.prodMap ⟨_, add_left_injective (n - k)⟩ (Embedding.refl ℕ)) := by
  ext ⟨i, j⟩
  suffices i + j = n ∧ j ≤ ki + j = n ∧ j ≤ k ↔ ∃ a, a + j = k ∧ a + (n - k) = i by simpa
  refine ⟨fun hi ↦ ⟨k - j, tsub_add_cancel_of_le hi.2, ?_⟩, ?_⟩
  · rw [add_comm, tsub_add_eq_add_tsub h, ← hi.1, add_assoc, Nat.add_sub_of_le hi.2,
      add_tsub_cancel_right]
  · rintro ⟨l, hl, rfl⟩
    refine ⟨?_, hl ▸ Nat.le_add_left j l⟩
    rw [add_assoc, add_comm, add_assoc, add_comm j l, hl]
    exact Nat.sub_add_cancel h

Filtered Antidiagonal by Upper Bound on Second Component: $\{(i,j) \mid i + j = n \text{ and } j \leq k\} = \{(i + (n - k), j) \mid i + j = k\}$

Informal description

For any natural numbers $n$ and $k$ with $k \leq n$, the subset of the antidiagonal $\{(i,j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n \text{ and } j \leq k\}$ is equal to the image of the antidiagonal of $k$ under the injective map $(i,j) \mapsto (i + (n - k), j)$.

Finset.Nat.antidiagonal_filter_fst_le_of_le theorem

 {n k : ℕ} (h : k ≤ n) :
  {a ∈ antidiagonal n | a.fst ≤ k} =
    (antidiagonal k).map (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective (n - k)⟩)

Full source

@[simp] lemma antidiagonal_filter_fst_le_of_le {n k : ℕ} (h : k ≤ n) :
    {a ∈ antidiagonal n | a.fst ≤ k} = (antidiagonal k).map
      (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective (n - k)⟩) := by
  have aux₁ : fun a ↦ a.fst ≤ k = (fun a ↦ a.snd ≤ k) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
  have aux₂ : ∀ i j, (∃ a b, a + b = k ∧ b = i ∧ a + (n - k) = j) ↔
                      ∃ a b, a + b = k ∧ a = i ∧ b + (n - k) = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
  rw [← map_prodComm_antidiagonal]
  simp_rw [aux₁, ← map_filter, antidiagonal_filter_snd_le_of_le h, map_map]
  ext ⟨i, j⟩
  simpa using aux₂ i j

Filtered Antidiagonal by Upper Bound on First Component: $\{(i,j) \mid i + j = n \text{ and } i \leq k\} = \{(i, j + (n - k)) \mid i + j = k\}$

Informal description

For any natural numbers $n$ and $k$ with $k \leq n$, the subset of the antidiagonal $\{(i,j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n \text{ and } i \leq k\}$ is equal to the image of the antidiagonal of $k$ under the injective map $(i,j) \mapsto (i, j + (n - k))$.

Finset.Nat.antidiagonal_filter_le_fst_of_le theorem

 {n k : ℕ} (h : k ≤ n) :
  {a ∈ antidiagonal n | k ≤ a.fst} =
    (antidiagonal (n - k)).map (Embedding.prodMap ⟨_, add_left_injective k⟩ (Embedding.refl ℕ))

Full source

@[simp] lemma antidiagonal_filter_le_fst_of_le {n k : ℕ} (h : k ≤ n) :
    {a ∈ antidiagonal n | k ≤ a.fst} = (antidiagonal (n - k)).map
      (Embedding.prodMap ⟨_, add_left_injective k⟩ (Embedding.refl ℕ)) := by
  ext ⟨i, j⟩
  suffices i + j = n ∧ k ≤ ii + j = n ∧ k ≤ i ↔ ∃ a, a + j = n - k ∧ a + k = i by simpa
  refine ⟨fun hi ↦ ⟨i - k, ?_, tsub_add_cancel_of_le hi.2⟩, ?_⟩
  · rw [← Nat.sub_add_comm hi.2, hi.1]
  · rintro ⟨l, hl, rfl⟩
    refine ⟨?_, Nat.le_add_left k l⟩
    rw [add_right_comm, hl]
    exact tsub_add_cancel_of_le h

Filtered Antidiagonal by Lower Bound on First Component: $\{(i,j) \mid i + j = n \text{ and } k \leq i\} = \{(i + k, j) \mid i + j = n - k\}$

Informal description

For any natural numbers $n$ and $k$ with $k \leq n$, the subset of the antidiagonal $\{(i,j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n \text{ and } k \leq i\}$ is equal to the image of the antidiagonal of $n - k$ under the injective map $(i,j) \mapsto (i + k, j)$.

Finset.Nat.antidiagonal_filter_le_snd_of_le theorem

 {n k : ℕ} (h : k ≤ n) :
  {a ∈ antidiagonal n | k ≤ a.snd} =
    (antidiagonal (n - k)).map (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective k⟩)

Full source

@[simp] lemma antidiagonal_filter_le_snd_of_le {n k : ℕ} (h : k ≤ n) :
    {a ∈ antidiagonal n | k ≤ a.snd} = (antidiagonal (n - k)).map
      (Embedding.prodMap (Embedding.refl ℕ) ⟨_, add_left_injective k⟩) := by
  have aux₁ : fun a ↦ k ≤ a.snd = (fun a ↦ k ≤ a.fst) ∘ (Equiv.prodComm ℕ ℕ).symm := rfl
  have aux₂ : ∀ i j, (∃ a b, a + b = n - k ∧ b = i ∧ a + k = j) ↔
                      ∃ a b, a + b = n - k ∧ a = i ∧ b + k = j :=
    fun i j ↦ by rw [exists_comm]; exact exists₂_congr (fun a b ↦ by rw [add_comm])
  rw [← map_prodComm_antidiagonal]
  simp_rw [aux₁, ← map_filter, antidiagonal_filter_le_fst_of_le h, map_map]
  ext ⟨i, j⟩
  simpa using aux₂ i j

Filtered Antidiagonal by Lower Bound on Second Component: $\{(i,j) \mid i + j = n \text{ and } k \leq j\} = \{(i, j + k) \mid i + j = n - k\}$

Informal description

For any natural numbers $n$ and $k$ with $k \leq n$, the subset of the antidiagonal $\{(i,j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n \text{ and } k \leq j\}$ is equal to the image of the antidiagonal of $n - k$ under the injective map $(i,j) \mapsto (i, j + k)$.

Finset.Nat.antidiagonalEquivFin definition

(n : ℕ) : antidiagonal n ≃ Fin (n + 1)

Full source

/-- The set `antidiagonal n` is equivalent to `Fin (n+1)`, via the first projection. -/
@[simps]
def antidiagonalEquivFin (n : ℕ) : antidiagonalantidiagonal n ≃ Fin (n + 1) where
  toFun := fun ⟨⟨i, _⟩, h⟩ ↦ ⟨i, antidiagonal.fst_lt h⟩
  invFun := fun ⟨i, h⟩ ↦ ⟨⟨i, n - i⟩, by
    rw [mem_antidiagonal, add_comm, Nat.sub_add_cancel]
    exact Nat.le_of_lt_succ h⟩
  left_inv := by rintro ⟨⟨i, j⟩, h⟩; ext; rfl
  right_inv _ := rfl

Bijection between antidiagonal pairs and finite indices

Informal description

For any natural number $n$, there is a bijection between the antidiagonal set $\text{antidiagonal}(n) = \{(i, j) \in \mathbb{N} \times \mathbb{N} \mid i + j = n\}$ and the finite type $\text{Fin}(n + 1)$. The bijection maps a pair $(i, j)$ to $i$ and its inverse maps an index $i$ to the pair $(i, n - i)$.

Notes