List.Nat.nodup_antidiagonal
theorem List.Nat.nodup_antidiagonal : ∀ (n : ℕ), (List.Nat.antidiagonal n).Nodup
The theorem `List.Nat.nodup_antidiagonal` states that for any natural number `n`, the antidiagonal of `n` does not contain any duplicate entries. The antidiagonal of `n` is defined as the list of pairs `(i, j)` such that `i + j = n`. Therefore, this theorem is asserting that no two pairs `(i, j)` and `(k, l)` where `i + j = n` and `k + l = n`, can both exist in the antidiagonal of `n` if `i = k` and `j = l`.
More concisely: For any natural number `n`, the antidiagonal of length `n` in the cartesian product of `n+1` copies of the natural numbers does not contain duplicate pairs.
|
List.Nat.mem_antidiagonal
theorem List.Nat.mem_antidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ List.Nat.antidiagonal n ↔ x.1 + x.2 = n
The theorem `List.Nat.mem_antidiagonal` states that for any natural number `n` and any pair of natural numbers `x`, the pair `x` is in the antidiagonal of `n` if and only if the sum of the elements in the pair equals `n`. In other words, a pair `(i, j)` of natural numbers belongs to the antidiagonal of a natural number `n` precisely when `i + j` is equal to `n`.
More concisely: The antidiagonal of a natural number `n` is precisely the set of pairs `(i, j)` of natural numbers such that `i + j = n`.
|
List.Nat.length_antidiagonal
theorem List.Nat.length_antidiagonal : ∀ (n : ℕ), (List.Nat.antidiagonal n).length = n + 1
This theorem states that the length of the antidiagonal of a natural number `n` is `n + 1`. In other words, if you create a list of pairs `(i, j)` where each pair sums up to `n`, the total number of such pairs will be `n + 1`. This list of pairs is referred to as the "antidiagonal" of `n`.
More concisely: The number of pairs (i, j) with i, j natural numbers and i + j = n is n + 1.
|
List.Nat.antidiagonal_zero
theorem List.Nat.antidiagonal_zero : List.Nat.antidiagonal 0 = [(0, 0)]
The theorem `List.Nat.antidiagonal_zero` states that the antidiagonal of the natural number `0` is the list containing just one pair `(0, 0)`. Here, the antidiagonal of a natural number `n` is defined as the list of pairs of natural numbers `(i, j)` such that `i + j = n`. In the case of `n = 0`, there's only one such pair, namely `(0, 0)`.
More concisely: The antidiagonal of natural number 0 is the list containing the single pair (0, 0).
|