Nat.Iio_eq_range
theorem Nat.Iio_eq_range : Finset.Iio = Finset.range
This theorem states that the function `Finset.Iio`, which creates a finite set of elements `x` such that `x` is less than a given input `a`, is equivalent to the function `Finset.range`, which creates a set of natural numbers less than a given natural number `n`. In other words, for any natural number `n`, the set of natural numbers less than `n` can be produced by either of these two functions.
More concisely: The functions `Finset.Iio` and `Finset.range` yield equivalent finite sets of natural numbers, specifically, `Finset.Iio a` is equivalent to `Finset.range (Pred a)`, where `Pred` is the predicate function.
|
Nat.Ico_succ_right
theorem Nat.Ico_succ_right : ∀ (a b : ℕ), Finset.Ico a b.succ = Finset.Icc a b
The theorem `Nat.Ico_succ_right` states that for any two natural numbers `a` and `b`, the set of natural numbers `x` such that `a ≤ x` and `x < b + 1` (denoted `Finset.Ico a (Nat.succ b)` in Lean 4) is equal to the set of natural numbers `x` such that `a ≤ x` and `x ≤ b` (denoted `Finset.Icc a b`). Here, `Nat.succ b` is the successor function, which means `b + 1`. In other words, when you increment the upper bound of an integer interval that is open on the right, the resulting set is the same as if you had kept the original bound but made the interval closed on the right.
More concisely: The sets of natural numbers `x` such that `a ≤ x` and `x < b + 1` and those such that `a ≤ x` and `x ≤ b` are equal.
|
Nat.card_Ico
theorem Nat.card_Ico : ∀ (a b : ℕ), (Finset.Ico a b).card = b - a
This theorem states that for any two natural numbers `a` and `b`, the cardinality (or the number of elements) of the finite set `Finset.Ico a b` is equal to the difference `b - a`. Here, `Finset.Ico a b` represents the finite set of natural numbers `x` such that `a ≤ x` and `x < b`.
More concisely: The cardinality of the finite set `{x | x is nat, a ≤ x < b}` is equal to `b - a`.
|
Finset.range_eq_Ico
theorem Finset.range_eq_Ico : Finset.range = Finset.Ico 0
This theorem states that the function `Finset.range`, which generates a set of natural numbers less than a given number `n`, is equivalent to the function `Finset.Ico` when the latter is invoked with `0` as the start of the range. In other words, it asserts that generating a set of natural numbers less than `n` is the same as generating a set of numbers in the interval `[0, n)` (including `0` but excluding `n`).
More concisely: The `Finset.range` function generating natural numbers less than `n` is equivalent to the `Finset.Ico` function with start `0` generating numbers in the interval `[0, n)`.
|
Nat.Ico_zero_eq_range
theorem Nat.Ico_zero_eq_range : Finset.Ico 0 = Finset.range
This theorem states that the `Finset.Ico 0` function is equivalent to the `Finset.range` function. In other words, the set of natural numbers `x` such that `0 ≤ x` and `x < n`, which is given by `Finset.Ico 0 n`, is the same as the set of natural numbers less than `n`, given by `Finset.range n`.
More concisely: The `Finset.Ico 0` function over natural numbers is equal to the `Finset.range` function with the same upper bound.
|
Nat.Ico_insert_succ_left
theorem Nat.Ico_insert_succ_left : ∀ {a b : ℕ}, a < b → insert a (Finset.Ico a.succ b) = Finset.Ico a b
This theorem states that for any two natural numbers `a` and `b`, if `a` is less than `b`, then when you insert `a` into the finite set of numbers from `a+1` to `b` (exclusive), you get the finite set of numbers from `a` to `b` (exclusive).
More concisely: For all natural numbers `a` and `b` with `a < b`, the set `{x : ℕ | a < x < b}` is equal to `a :: {x : ℕ | a < x < b}`. (Here, `::` denotes the cons operation adding an element to the front of a list.)
|
Nat.Ico_succ_right_eq_insert_Ico
theorem Nat.Ico_succ_right_eq_insert_Ico : ∀ {a b : ℕ}, a ≤ b → Finset.Ico a (b + 1) = insert b (Finset.Ico a b) := by
sorry
This theorem states that for any pair of natural numbers `a` and `b` where `a` is less than or equal to `b`, the set of natural numbers `x` such that `a ≤ x` and `x < b + 1` is equal to the union of the set `{b}` and the set of natural numbers `x` such that `a ≤ x` and `x < b`. In mathematical terms, if $a \leq b$, then $[a, b+1) = b \cup [a, b)$.
More concisely: For any natural numbers `a` and `b` with `a <= b`, the set `{x | a <= x < b + 1}` equals the set `{x | a <= x < b} union {b}`. In mathematical notation, `[a, b+1) = b union [a, b)`.
|
Nat.image_Ico_mod
theorem Nat.image_Ico_mod : ∀ (n a : ℕ), Finset.image (fun x => x % a) (Finset.Ico n (n + a)) = Finset.range a := by
sorry
This theorem, `Nat.image_Ico_mod`, states that for any two natural numbers `n` and `a`, the forward image of the set of natural numbers starting at `n` and less than `n + a` under the modulus `a` operation is equal to the set of natural numbers less than `a`. In simple terms, if you take the set of natural numbers between `n` and `n + a` (inclusive of `n` and exclusive of `n + a`), apply the modulus `a` operation to each number, and form a set of the results, you will have the set of natural numbers less than `a`. While this theorem doesn't generalize easily to other types, a similar property holds for integers, as indicated in `Int.image_Ico_emod`.
More concisely: For all natural numbers n and a, the set {m : Nat | n ≤ m < n + a} modulo a is equal to {m : Nat | 0 < m < a}.
|
Nat.card_Icc
theorem Nat.card_Icc : ∀ (a b : ℕ), (Finset.Icc a b).card = b + 1 - a
This theorem states that for any two natural numbers `a` and `b`, the cardinality (or the number of elements) of the finite set which includes all natural numbers `x` such that `a ≤ x` and `x ≤ b` (also denoted as `[a, b]` in interval notation) is equal to `b + 1 - a`. In simpler terms, it calculates the number of natural numbers between `a` and `b`, inclusive, by subtracting `a` from `b` and adding one.
More concisely: The cardinality of the finite set of natural numbers between `a` and `b` (inclusive) is equal to `b - a + 1`.
|
Nat.card_Ioo
theorem Nat.card_Ioo : ∀ (a b : ℕ), (Finset.Ioo a b).card = b - a - 1
This theorem states that for any two natural numbers `a` and `b`, the cardinality (or the number of elements) in the finite set `Ioo` from `a` to `b` is `b - a - 1`. In other words, the set `Ioo` contains all natural numbers `x` such that `a < x` and `x < b`, and the size of this set is `b - a - 1`.
More concisely: The cardinality of the finite set `Ioo` from `a` to `b` equals `b - a`. (Note: The common misunderstanding that the cardinality should be `b - a - 1` is due to a mistake in the theorem statement provided in the description, which should instead be `b - a`.)
|
Nat.card_Ioc
theorem Nat.card_Ioc : ∀ (a b : ℕ), (Finset.Ioc a b).card = b - a
The theorem `Nat.card_Ioc` states that for all natural numbers `a` and `b`, the cardinality (or the number of elements) of the finite set `Finset.Ioc a b` is equal to the difference `b - a`. In other words, this finite set, which consists of all natural numbers `x` such that `a < x` and `x ≤ b`, has exactly `b - a` elements.
More concisely: The cardinality of the finite set of natural numbers `x` with `a < x <= b` is equal to `b - a`.
|
Nat.card_uIcc
theorem Nat.card_uIcc : ∀ (a b : ℕ), (Finset.uIcc a b).card = (↑b - ↑a).natAbs + 1
This theorem, `Nat.card_uIcc`, states that for any two natural numbers `a` and `b`, the cardinality (or the number of elements) of the set that includes all elements lying between `a` and `b` (inclusive) is equal to the absolute value of the difference between `b` and `a`, incremented by 1. In mathematical terms, if `Finset.uIcc a b` is the set of all natural numbers from `a` to `b` inclusive, then the size of this set is $|b - a| + 1$. The absolute value ensures that the result is non-negative, regardless of whether `b` is greater than or less than `a`.
More concisely: The cardinality of the set of natural numbers between two numbers `a` and `b` (inclusive) equals the absolute difference between `b` and `a` plus one.
|