Multiset.Nat.card_antidiagonal
theorem Multiset.Nat.card_antidiagonal : ∀ (n : ℕ), Multiset.card (Multiset.Nat.antidiagonal n) = n + 1
The theorem `Multiset.Nat.card_antidiagonal` states that for any natural number `n`, the cardinality (or the count of the number of elements) of the antidiagonal of `n` is `n + 1`. Here, the antidiagonal of `n` is defined as a multiset of pairs `(i, j)` where `i + j` equals `n`. Thus, the theorem asserts that there are exactly `n + 1` such pairs in the antidiagonal of any natural number `n`.
More concisely: The cardinality of the antidiagonal of a natural number `n` as a multiset of pairs `(i, j)` with `i + j = n` is `n + 1`.
|
Multiset.Nat.nodup_antidiagonal
theorem Multiset.Nat.nodup_antidiagonal : ∀ (n : ℕ), (Multiset.Nat.antidiagonal n).Nodup
The theorem states that the antidiagonal of a natural number `n` does not contain any duplicate entries. In other words, for every natural number `n`, the multiset of all pairs `(i, j)` such that `i + j = n` - referred to as the antidiagonal of `n` - is a multiset with no repeated elements.
More concisely: For all natural numbers n, the multiset of pairs (i, j) with i + j = n has no repeated elements.
|
Multiset.Nat.mem_antidiagonal
theorem Multiset.Nat.mem_antidiagonal : ∀ {n : ℕ} {x : ℕ × ℕ}, x ∈ Multiset.Nat.antidiagonal n ↔ x.1 + x.2 = n := by
sorry
The theorem `Multiset.Nat.mem_antidiagonal` states that for a given natural number `n` and a pair of natural numbers `(i, j)`, the pair `(i, j)` is included in the antidiagonal of `n` if and only if the sum of `i` and `j` equals `n`. The antidiagonal of a natural number `n` is defined as the multiset of all pairs `(i, j)` where `i + j = n`.
More concisely: A pair (i, j) is in the antidiagonal of a natural number n if and only if i + j = n.
|
Multiset.Nat.antidiagonal_zero
theorem Multiset.Nat.antidiagonal_zero : Multiset.Nat.antidiagonal 0 = {(0, 0)}
The theorem `Multiset.Nat.antidiagonal_zero` states that the antidiagonal of `0` is a multiset consisting only of the pair `(0, 0)`. In other words, the only pair of natural numbers `(i, j)` that can sum up to `0` is `(0, 0)`.
More concisely: The theorem `Multiset.Nat.antidiagonal_zero` asserts that the multiset of natural number pairs with equal sum equal to zero only contains the single element `(0, 0)`.
|