Finset.Nat.card_antidiagonal
theorem Finset.Nat.card_antidiagonal : ∀ (n : ℕ), (Finset.antidiagonal n).card = n + 1
This theorem states that for any natural number `n`, the cardinality (or size) of its antidiagonal set is `n + 1`. In other words, if you create an antidiagonal set from a natural number `n`, there will be `n + 1` elements in that set.
More concisely: For any natural number `n`, the size of its antidiagonal set is `n + 1`.
|
Finset.Nat.antidiagonal_zero
theorem Finset.Nat.antidiagonal_zero : Finset.antidiagonal 0 = {(0, 0)}
This theorem states that the antidiagonal of 0, when computed using the `Finset.antidiagonal` function in Lean 4, is the singleton set containing the pair `(0, 0)`. The antidiagonal of a number n is generally a set of pairs `(a, b)` such that `a + b = n`, so this result is consistent with that definition since `0 + 0 = 0`.
More concisely: The antidiagonal of 0, as computed in Lean 4 using `Finset.antidiagonal`, is the set {(0, 0)}.
|