Nat.choose_symm
theorem Nat.choose_symm : ∀ {n k : ℕ}, k ≤ n → n.choose (n - k) = n.choose k
This theorem states that for any two natural numbers `n` and `k`, where `k` is less than or equal to `n`, the number of `k`-element subsets in an `n`-element set (denoted as `Nat.choose n k`) is the same as the number of `(n - k)`-element subsets in the same `n`-element set (denoted as `Nat.choose n (n - k)`). In other words, the binomial coefficient ${n \choose k}$ is equal to ${n \choose n-k}$ for any `n` and `k` such that `k` is less than or equal to `n`. This represents the symmetry property of binomial coefficients.
More concisely: For any natural number `n` and `k` with `k` less than or equal to `n`, the number of `k`-element subsets in an `n`-element set equals the number of `(n - k)`-element subsets, i.e., `Nat.choose n k = Nat.choose n (n - k)`.
|
Nat.choose_succ_self
theorem Nat.choose_succ_self : ∀ (n : ℕ), n.choose n.succ = 0
The theorem `Nat.choose_succ_self` states that for any natural number `n`, the binomial coefficient or "choose" operation of `n` and `n + 1`, denoted as `Nat.choose n (Nat.succ n)`, is always equal to zero. In other words, there are no ways to choose `n + 1` items from a set of `n` items, which intuitively makes sense since the set does not contain `n + 1` items.
More concisely: For all natural numbers n, the binomial coefficient Nat.choose n (Nat.succ n) equals zero.
|
Nat.choose_mul_factorial_mul_factorial
theorem Nat.choose_mul_factorial_mul_factorial :
∀ {n k : ℕ}, k ≤ n → n.choose k * k.factorial * (n - k).factorial = n.factorial
The theorem `Nat.choose_mul_factorial_mul_factorial` states that for any natural numbers `n` and `k` where `k` is less than or equal to `n`, the product of the binomial coefficient of `n` choose `k`, the factorial of `k`, and the factorial of `n - k` is equal to the factorial of `n`. In mathematical notation, this theorem can be expressed as: $\binom{n}{k} * k! * (n-k)! = n!$ for $k \leq n$.
More concisely: For any natural numbers $n$ and $k$ with $k \leq n$, $\binom{n}{k} \cdot k! \cdot (n-k)! = n!$.
|
Nat.choose_le_middle
theorem Nat.choose_le_middle : ∀ (r n : ℕ), n.choose r ≤ n.choose (n / 2)
The theorem `Nat.choose_le_middle` states that for any two natural numbers `r` and `n`, the binomial coefficient ("n choose r") is always less than or equal to the binomial coefficient when choosing half of `n` (i.e., "n choose n/2"). This theorem essentially suggests that the binomial coefficient is maximized when the number of elements chosen is half the total number of elements.
More concisely: For all natural numbers r and n, the binomial coefficient n choose r is less than or equal to n choose n/2.
|
Nat.choose_zero_right
theorem Nat.choose_zero_right : ∀ (n : ℕ), n.choose 0 = 1
The theorem `Nat.choose_zero_right` states that for any natural number `n`, the number of ways to choose zero elements from a set with `n` elements is always 1. This is a specific case of the general binomial coefficient concept, where choosing no elements from any set results in one possibility, which is the empty set.
More concisely: For any natural number `n`, there is exactly 1 way to choose 0 elements from a set of size `n`.
|
Nat.choose_one_right
theorem Nat.choose_one_right : ∀ (n : ℕ), n.choose 1 = n
The theorem `Nat.choose_one_right` states that for any natural number `n`, the binomial coefficient `Nat.choose n 1` (also known as "n choose 1") is equal to `n` itself. In other words, the number of distinct subsets of size 1 that can be formed from a set of `n` elements is just `n`. This is naturally true because, for a given set of `n` elements, we can form `n` different one-element subsets, each containing a different element of the set.
More concisely: For any natural number `n`, the binomial coefficient `Nat.choose n 1` equals `n`. Alternatively, the number of subsets of size 1 in a set of `n` elements is `n`.
|
Nat.choose_pos
theorem Nat.choose_pos : ∀ {n k : ℕ}, k ≤ n → 0 < n.choose k
This theorem, `Nat.choose_pos`, states that for all natural numbers `n` and `k`, if `k` is less than or equal to `n`, then the value of the binomial coefficient `Nat.choose n k` (the number of ways to choose `k` elements from a set of `n` elements) is greater than zero. In other words, if we have a set of `n` elements and we want to choose `k` elements from it, there is at least one way to do this as long as `k` is less than or equal to `n`.
More concisely: For all natural numbers n and k with k ≤ n, Nat.choose n k is a positive natural number.
|
Nat.choose_succ_right_eq
theorem Nat.choose_succ_right_eq : ∀ (n k : ℕ), n.choose (k + 1) * (k + 1) = n.choose k * (n - k)
The theorem `Nat.choose_succ_right_eq` states that for all natural numbers `n` and `k`, the binomial coefficient of `n` choose `(k + 1)`, multiplied by `(k + 1)`, is equal to the binomial coefficient of `n` choose `k`, multiplied by `(n - k)`. In mathematical notation, this is expressed as $\binom{n}{k+1} \cdot (k+1) = \binom{n}{k} \cdot (n - k)$. This theorem is a relation between consecutive binomial coefficients.
More concisely: The theorem asserts that for all natural numbers n and k, the product of the binomial coefficient of n choose k+1 and k+1 equals the product of the binomial coefficient of n choose k and (n-k). In other words, $\binom{n}{k+1} \cdot (k+1) = \binom{n}{k} \cdot (n-k)$.
|
Nat.descFactorial_eq_factorial_mul_choose
theorem Nat.descFactorial_eq_factorial_mul_choose : ∀ (n k : ℕ), n.descFactorial k = k.factorial * n.choose k := by
sorry
The theorem `Nat.descFactorial_eq_factorial_mul_choose` states that for any two natural numbers `n` and `k`, the descending factorial of `n` taken `k` at a time is equal to the product of the factorial of `k` and the binomial coefficient of `n` choose `k`. In mathematical terms, it expresses the equality `n.descFactorial k = k! * (n choose k)`. This theorem is a relationship between factorials, binomial coefficients, and descending factorials in combinatorial mathematics.
More concisely: For any natural numbers `n` and `k`, the descending factorial of `n` taken `k` at a time equals the product of the factorial of `k` and the binomial coefficient of `n` choose `k`: `n.descFactorial k = k! * (n choose k)`.
|
Nat.multichoose_zero_right
theorem Nat.multichoose_zero_right : ∀ (n : ℕ), n.multichoose 0 = 1
The theorem `Nat.multichoose_zero_right` states that for any natural number `n`, the multiset choosing function `Nat.multichoose` with `n` as the size of the type and `0` as the cardinality of the multiset always equals `1`. In mathematical terms, this theorem says that there is exactly one way to choose a multiset of size `0` from a set of size `n`, for any `n`, and that is the empty set.
More concisely: For any natural number `n`, the multiset choosing function `Nat.multichoose` with `n` as the size and `0` as the cardinality equals 1, equivalent to there being only one multiset of size 0 from a set of size `n`, which is the empty multiset.
|
Nat.choose_symm_add
theorem Nat.choose_symm_add : ∀ {a b : ℕ}, (a + b).choose a = (a + b).choose b
This theorem, `Nat.choose_symm_add`, states that for all natural numbers `a` and `b`, the number of ways to choose `a` elements from a set of `a + b` elements is equal to the number of ways to choose `b` elements from the same set. In other words, the binomial coefficient ${a + b \choose a}$ is equal to ${a + b \choose b}$. This property is a reflection of the symmetry in the definition of binomial coefficients.
More concisely: For all natural numbers a and b, the number of ways to choose a elements from a set of size a + b is equal to the number of ways to choose b elements from the same set. Equivalently, (a + b) choose a = (a + b) choose b.
|
Nat.choose_le_succ_of_lt_half_left
theorem Nat.choose_le_succ_of_lt_half_left : ∀ {r n : ℕ}, r < n / 2 → n.choose r ≤ n.choose (r + 1)
This theorem demonstrates that the binomial coefficient function, represented as `Nat.choose` in Lean 4, is an increasing function for smaller values of the second argument. In more detail, for every pair of natural numbers `n` and `r` such that `r` is less than half of `n`, the binomial coefficient `n.choose r` is less than or equal to `n.choose (r + 1)`.
More concisely: For all natural numbers `n` and `r` with `r < n / 2`, the binomial coefficient `n choose r` is less than or equal to `n choose (r + 1)`.
|
Nat.choose_eq_factorial_div_factorial
theorem Nat.choose_eq_factorial_div_factorial :
∀ {n k : ℕ}, k ≤ n → n.choose k = n.factorial / (k.factorial * (n - k).factorial)
This theorem states that for any two natural numbers `n` and `k`, where `k` is less than or equal to `n`, the binomial coefficient `n choose k` is equal to the division of the factorial of `n` by the product of the factorial of `k` and the factorial of `n - k`. This result is often used in combinatorics and probability theory. It is mathematically expressed as $\binom{n}{k} = \frac{n!}{k!(n-k)!}$.
More concisely: The binomial coefficient `n choose k` is equal to the ratio of `n!` to the product of `k!` and `(n-k)!`.
|
Nat.choose_self
theorem Nat.choose_self : ∀ (n : ℕ), n.choose n = 1
The theorem `Nat.choose_self` states that for any natural number `n`, the number of `n`-element subsets in an `n`-element set, also known as the binomial coefficient, is 1. In other words, it states that there is only one way to choose `n` elements from a set of `n` elements, which makes sense because the only possible subset is the set itself.
More concisely: The theorem `Nat.choose_self` asserts that for any natural number `n`, the number of `n`-element subsets of a set with `n` elements is equal to 1.
|
Nat.choose_two_right
theorem Nat.choose_two_right : ∀ (n : ℕ), n.choose 2 = n * (n - 1) / 2
This theorem states that choosing 2 elements from a set of size `n` is equivalent to the `n`-th triangle number, which is calculated as `n * (n - 1) / 2`. In other words, the number of ways to pick two items from `n` without regard to order is the same as the `n`-th triangular number.
More concisely: The number of ways to choose 2 elements from a set of size `n` is equal to the `n`-th triangular number `n * (n - 1) / 2`.
|
Nat.choose_eq_zero_of_lt
theorem Nat.choose_eq_zero_of_lt : ∀ {n k : ℕ}, n < k → n.choose k = 0
The theorem `Nat.choose_eq_zero_of_lt` states that for all natural numbers `n` and `k`, if `n` is less than `k`, then the binomial coefficient `Nat.choose n k` is equal to zero. In other words, it's not possible to choose `k` elements from a set of `n` elements if `k` is greater than `n`, and thus the number of ways to do so is zero. This aligns with the common combinatorial understanding that there are zero ways to choose more items than are available in the set.
More concisely: For all natural numbers n and k, if n < k then Nat.choose n k = 0.
|
Nat.factorial_mul_factorial_dvd_factorial
theorem Nat.factorial_mul_factorial_dvd_factorial :
∀ {n k : ℕ}, k ≤ n → k.factorial * (n - k).factorial ∣ n.factorial
The theorem `Nat.factorial_mul_factorial_dvd_factorial` states that for any two natural numbers `n` and `k` where `k` is less than or equal to `n`, the product of the factorial of `k` and the factorial of the difference between `n` and `k`, divides the factorial of `n`. This can be written in mathematical notation as: if $0 \leq k \leq n$, then $k! \cdot (n - k)!$ divides $n!$.
More concisely: For any natural numbers $n \geq k \geq 0$, $k! \cdot (n-k)!$ divides $n!$.
|
Nat.choose_succ_succ
theorem Nat.choose_succ_succ : ∀ (n k : ℕ), n.succ.choose k.succ = n.choose k + n.choose k.succ
The theorem `Nat.choose_succ_succ` is about binomial coefficients (commonly denoted by "n choose k") in combinatorics. It states that for all natural numbers `n` and `k`, the binomial coefficient of `n+1` choose `k+1` is equal to the sum of the binomial coefficient of `n` choose `k` and the binomial coefficient of `n` choose `k+1`. In other words, this theorem is a formalization of the Pascal's Rule, which is a fundamental property of binomial coefficients used in combinatorial mathematics. The theorem may be written in LaTeX mathematics as: $\binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1}$.
More concisely: The theorem `Nat.choose_succ_succ` in Lean 4 states that for all natural numbers `n` and `k`, the binomial coefficient of `n+1` choose `k+1` equals the sum of the binomial coefficients of `n` choose `k` and `n` choose `k+1`. In mathematical notation, $\binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1}$.
|