Fin.natAdd_cast
theorem Fin.natAdd_cast :
∀ {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n), Fin.natAdd m (Fin.cast h i) = Fin.cast ⋯ (Fin.natAdd m i) := by
sorry
The theorem `Fin.natAdd_cast` states that for all natural numbers `n`, `n'`, and `m`, and for all `i` of type `Fin n'` where `n'` equals `n`, the operation of adding `m` to `i` "on the left" (represented by `Fin.natAdd m`) before casting `i` to an equal `Fin` type (via `Fin.cast h`) is equivalent to adding `m` to `i` "on the left" after casting `i`. In other words, the `Fin.natAdd` operation and the `Fin.cast` operation commute with each other. This can be useful for rewriting expressions in Lean 4.
More concisely: For all natural numbers `n`, `n'`, `m`, and `i` of type `Fin n` with `n' = n`, the application of `Fin.cast` to `i` and the addition of `m` to `i` (on the left) commute. In other words, `Fin.natAdd m (Fin.cast i) = Fin.cast (Fin.natAdd m i)`.
|
Fin.addCases_left
theorem Fin.addCases_left :
∀ {m n : ℕ} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (Fin.castAdd n i)}
{right : (i : Fin n) → motive (Fin.natAdd m i)} (i : Fin m), Fin.addCases left right (Fin.castAdd n i) = left i
The theorem `Fin.addCases_left` states that for any natural numbers `m` and `n`, for any `motive` which is a type dependent on a `Fin (m + n)`, and for any `left` function mapping from `Fin m` to this `motive` and a `right` function mapping from `Fin n` to this `motive`, applying `Fin.addCases` to `left`, `right` and `Fin.castAdd n i` (where `i` is a `Fin m`) results in the same output as applying `left` to `i`. In essence, this theorem asserts that `Fin.addCases` applied to a value obtained by extending the range of `i` using `Fin.castAdd` is equivalent to just applying the `left` function to the original `i`.
More concisely: For any natural numbers m and n, and any type-dependent motive, the application of Fin.addCases to left functions mapping from Fin m and right functions mapping from Fin n, along with Fin.castAdd, is equivalent to simply applying the left function to elements of Fin m.
|
Fin.succ_lt_succ_iff
theorem Fin.succ_lt_succ_iff : ∀ {n : ℕ} {a b : Fin n}, a.succ < b.succ ↔ a < b
This theorem, named `Fin.succ_lt_succ_iff`, states that for all natural numbers `n` and for all elements `a` and `b` of the type `Fin n` (which represents the set of natural numbers less than `n`), the condition "the successor of `a` is less than the successor of `b`" is equivalent to the condition " `a` is less than `b`". In other words, the comparison of the order of `a` and `b` is the same whether we consider `a` and `b` themselves or their successors. This theorem is a formalization of the intuitive fact about the order of natural numbers.
More concisely: For all natural numbers `n` and `a`, `b` in `Fin n`, `a < b` if and only if `a.succ` is less than `b.succ`.
|
Fin.castAdd_zero
theorem Fin.castAdd_zero : ∀ {n : ℕ}, Fin.castAdd 0 = Fin.cast ⋯
The theorem `Fin.castAdd_zero` states that for all natural numbers `n`, the function `Fin.castAdd 0` is equal to the function `Fin.cast`. In simpler terms, it means that adding 0 to a finite set `Fin n` -- a procedure defined by `Fin.castAdd 0` -- is the same as casting `Fin n` to itself, which is the operation performed by the `Fin.cast` function. This theorem is a reflection of a basic arithmetic principle, that adding zero doesn't change the value of a number, adapted to the context of finite sets in Lean 4.
More concisely: For all natural numbers `n`, `Fin.castAdd 0 (Fin.cast n) = Fin.cast n`.
|
Fin.castSucc_lt_castSucc_iff
theorem Fin.castSucc_lt_castSucc_iff : ∀ {n : ℕ} {a b : Fin n}, a.castSucc < b.castSucc ↔ a < b
The theorem `Fin.castSucc_lt_castSucc_iff` states that for any natural number `n` and any two elements `a` and `b` of the finite set `Fin n`, the embedding of `a` into `Fin (n+1)` is less than the embedding of `b` into `Fin (n+1)` if and only if `a` is less than `b`. In other words, the order of elements is preserved when they are embedded from `Fin n` to `Fin (n+1)` via the `castSucc` function.
More concisely: For all natural numbers n and Fin n elements a and b, a < b if and only if castSucc a < castSucc b in Fin (n+1).
|
Fin.exists_castSucc_eq
theorem Fin.exists_castSucc_eq : ∀ {n : ℕ} {i : Fin (n + 1)}, (∃ j, j.castSucc = i) ↔ i ≠ Fin.last n
This theorem states that for any natural number `n` and any `i : Fin (n + 1)`, there exists a `j` such that `j` cast to `Fin (n + 1)` using `Fin.castSucc` equals `i` if and only if `i` is not the greatest value of `Fin (n+1)`. In other words, every element of `Fin (n + 1)` except for the highest one can be obtained by embedding some element of `Fin n` into `Fin (n + 1)` using the `Fin.castSucc` function.
More concisely: For any natural number `n` and `i : Fin (n + 1)` not equal to the greatest element, there exists a `j : Fin n` such that `i` is the image of `j` under the `Fin.castSucc` function.
|
Fin.forall_fin_succ
theorem Fin.forall_fin_succ :
∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∀ (i : Fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin n), P i.succ
The theorem `Fin.forall_fin_succ` states that for every natural number `n` and a property `P` that each element of the type `Fin (n + 1)` might have, the property `P` holds for all elements in `Fin (n + 1)` if and only if `P` holds for the zeroth element and for all elements in `Fin n` when they are passed through the function `Fin.succ`. The function `Fin.succ` takes an element of `Fin n` and returns an element of `Fin (n + 1)`, effectively shifting the index of the element by 1.
More concisely: For any natural number `n` and property `P`, `P` holds for all elements in `Fin (n + 1)` if and only if `P` holds for the zero element and for the successor of each element in `Fin n`.
|
Fin.addCases_right
theorem Fin.addCases_right :
∀ {m n : ℕ} {motive : Fin (m + n) → Sort u_1} {left : (i : Fin m) → motive (Fin.castAdd n i)}
{right : (i : Fin n) → motive (Fin.natAdd m i)} (i : Fin n), Fin.addCases left right (Fin.natAdd m i) = right i
The theorem `Fin.addCases_right` states that for any two natural numbers `m` and `n`, any motive (a function or property) depending on a finite ordinal of size `m + n`, and any definitions of this motive for finite ordinals smaller than `m` and `n` respectively, if we have a finite ordinal `i` less than `n`, then applying the function `Fin.addCases` with the motive, the definitions, and `i` after adding `m` to it through `Fin.natAdd`, will yield the same result as directly applying the second definition (`right`) to `i`. In other words, `Fin.addCases` correctly applies the second definition when the input is in the range of the second definition.
More concisely: For any natural numbers `m` and `n`, and any motive defined for finite ordinals less than `m + n`, applying `Fin.addCases` to the motive with definitions for `m` and `n` yields the same result as directly applying the definition for `n` to any finite ordinal less than `n`.
|
Fin.ext_iff
theorem Fin.ext_iff : ∀ {n : ℕ} {a b : Fin n}, a = b ↔ ↑a = ↑b
This theorem states that for any natural number `n` and any two elements `a` and `b` of the type `Fin n` (which represents a finite set of size `n`), `a` and `b` are equal if and only if their corresponding natural number representations (obtained by the coercion function `↑`) are also equal. In mathematical terms, it's saying that two elements of a finite set are equal if their corresponding indices in the set (from 0 to n-1) are the same.
More concisely: For any natural number `n` and elements `a` and `b` of `Fin n`, `a = b` if and only if `↑a = ↑b`.
|
Fin.val_add
theorem Fin.val_add : ∀ {n : ℕ} (a b : Fin n), ↑(a + b) = (↑a + ↑b) % n
This theorem, `Fin.val_add`, states that for any natural number `n` and any two finite numbers `a` and `b` (which are both less than `n`), the value obtained by casting the sum of `a` and `b` to a natural number is equal to the remainder when the sum of the natural number equivalents of `a` and `b` is divided by `n`. In essence, this theorem is about performing addition in the finite number system (modulo arithmetic) and making sure it corresponds correctly to the arithmetic in the natural numbers.
More concisely: For any natural number `n`, and finite numbers `a` and `b` less than `n`, the cast of `a + b` to a natural number equals the remainder when `a + b` is modulo `n`.
|
Fin.succ_inj
theorem Fin.succ_inj : ∀ {n : ℕ} {a b : Fin n}, a.succ = b.succ ↔ a = b
The theorem `Fin.succ_inj` states that for any natural number `n` and any two elements `a` and `b` of the finite set of natural numbers less than `n` (denoted as `Fin n`), the function `Fin.succ` being equal on `a` and `b` (i.e., `Fin.succ a = Fin.succ b`) is equivalent to `a` being equal to `b` (i.e., `a = b`). In other words, the function `Fin.succ`, which adds 1 to a given natural number while ensuring that the result is still less than the incremented natural number `n+1`, is injective (or one-to-one).
More concisely: The function `Fin.succ` from the finite set `Fin n` to itself is injective, i.e., `Fin.succ a = Fin.succ b` implies `a = b`.
|
Fin.succ_le_succ_iff
theorem Fin.succ_le_succ_iff : ∀ {n : ℕ} {a b : Fin n}, a.succ ≤ b.succ ↔ a ≤ b
The theorem `Fin.succ_le_succ_iff` states that for any natural number `n` and any two elements `a` and `b` of the finite set `Fin n`, the successor of `a` is less than or equal to the successor of `b` if and only if `a` is less than or equal to `b`. This theorem essentially asserts the preservation of the order relationship under the successor operation in the context of finite sets in Lean 4.
More concisely: For any natural number `n` and `a, b` in `Fin n`, `a < b` if and only if `succ a < succ b`.
|
Fin.castSucc_lt_iff_succ_le
theorem Fin.castSucc_lt_iff_succ_le : ∀ {n : ℕ} {i : Fin n} {j : Fin (n + 1)}, i.castSucc < j ↔ i.succ ≤ j
This theorem, `Fin.castSucc_lt_iff_succ_le`, states that for any natural number `n` and for any elements `i` from the Finset `Fin n` and `j` from the Finset `Fin (n + 1)`, the function `Fin.castSucc i` is less than `j` if and only if `Fin.succ i` is less than or equal to `j`. In other words, it's comparing the ordering relations after applying the `castSucc` and `succ` functions to `i`, in the context of the specific finite sets that `i` and `j` belong to.
More concisely: For any natural numbers `n`, `i ∈ Fin n`, and `j ∈ Fin (n + 1)`, `Fin.castSucc i < j` if and only if `Fin.succ i ≤ j`.
|
Fin.castAdd_cast
theorem Fin.castAdd_cast :
∀ {n n' : ℕ} (m : ℕ) (i : Fin n') (h : n' = n), Fin.castAdd m (Fin.cast h i) = Fin.cast ⋯ (Fin.castAdd m i) := by
sorry
The theorem `Fin.castAdd_cast` states that for any natural numbers `n`, `n'`, `m` and an instance `i` of `Fin n'`, along with a proof `h` that `n'` is equal to `n`, applying the function `Fin.cast` to the result of embedding `i` from `Fin n'` into `Fin (n + m)` using `Fin.castAdd` is the same as embedding `i` into `Fin (n' + m)` using `Fin.castAdd` and then applying `Fin.cast` to the result. This theorem facilitates the rewriting process in Lean 4, especially when you need to swap the order of `Fin.cast` and `Fin.castAdd`.
More concisely: For any natural numbers `n`, `n'`, `m`, and an equality proof `h` between `n'` and `n`, the application of `Fin.castAdd` followed by `Fin.cast` on an element `i : Fin n'` is equivalent to applying `Fin.cast` followed by `Fin.castAdd` on `i`. In other words, `Fin.cast (Fin.castAdd i (Fin.succ n)) = Fin.castAdd (Fin.cast i) (Fin.succ n)`.
|
Fin.is_le
theorem Fin.is_le : ∀ {n : ℕ} (i : Fin (n + 1)), ↑i ≤ n
This theorem states that for every natural number `n` and for every element `i` of the finite set of size `n + 1`, the value of `i` (when converted to a natural number) is less than or equal to `n`. In mathematical terms, for all natural numbers `n` and all `i` in the finite set of size `n+1`, it holds that `i ≤ n`.
More concisely: For every natural number `n` and every element `i` in a finite set of size `n+1`, `i` is less than or equal to `n`.
|
Fin.val_last
theorem Fin.val_last : ∀ (n : ℕ), ↑(Fin.last n) = n
This theorem, `Fin.val_last`, states that for every natural number `n`, the numerical value (obtained by using the coercion function `↑`) of the greatest value of `Fin (n+1)`, as defined by `Fin.last n`, is equal to `n` itself. In other words, when we consider the "last" element in the finite set of size `n+1`, its value is `n`. This is in line with the convention of starting indexing from 0 in Lean 4.
More concisely: For every natural number `n`, the greatest element in the finite set `Fin (n+1)` has value `n`.
|
Fin.le_last
theorem Fin.le_last : ∀ {n : ℕ} (i : Fin (n + 1)), i ≤ Fin.last n
The theorem `Fin.le_last` states that for any natural number `n` and any element `i` of the finite ordered set `Fin (n + 1)`, `i` is less than or equal to the greatest value of `Fin (n + 1)`, denoted as `Fin.last n`. In other words, all elements of the finite set `Fin (n + 1)` are less than or equal to the maximum element of that set.
More concisely: For any natural number `n` and element `i` of `Fin (n + 1)`, `i ≤ Fin.last n`.
|
Fin.coe_cast
theorem Fin.coe_cast : ∀ {n m : ℕ} (h : n = m) (i : Fin n), ↑(Fin.cast h i) = ↑i
The theorem `Fin.coe_cast` states that for any two natural numbers `n` and `m`, and for any equality `h` that asserts that `n` equals `m`, and for any value `i` in the finite set of natural numbers less than `n` (denoted `Fin n`), the coercion of `i` to a natural number remains the same after it is embedded into the finite set of natural numbers less than `m` via `Fin.cast` function using the equality `h`. In other words, the casting operation preserves the original numerical value of `i`.
More concisely: For any natural numbers `n`, `m`, equality `h` between `n` and `m`, and `i` in `Fin n`, the coercion of `i` to a natural number is equal to its coercion when embedded into `Fin m` via `Fin.cast` with `h`.
|
Fin.ext
theorem Fin.ext : ∀ {n : ℕ} {a b : Fin n}, ↑a = ↑b → a = b
The theorem `Fin.ext` states that for any natural number `n` and for any two objects `a` and `b` of the type `Fin n` (i.e., finite sets of size `n`), if their coercion to natural numbers (denoted by `↑a` and `↑b`) are equal, then `a` and `b` are also equal. In other words, two elements of a finite set of size `n` are identical if and only if their corresponding natural numbers are identical.
More concisely: For any natural number `n` and any `a, b : Fin n`, `a = b` if and only if `↑a = ↑b`.
|
Fin.castSucc_pos
theorem Fin.castSucc_pos : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → 0 < i.castSucc
The theorem `Fin.castSucc_pos` asserts that for any natural number `n` and any finite ordinal `i` within `n + 1`, if `i` is greater than zero, then `i.castSucc` is also greater than zero. `i.castSucc` is a function that casts `i` as a finite ordinal within a greater set, specifically, the set `n + 2`.
More concisely: For any natural number `n` and finite ordinal `i` within `n + 1` with `i` greater than zero, `i.castSucc` is a positive finite ordinal.
|
Fin.castSucc_fin_succ
theorem Fin.castSucc_fin_succ : ∀ (n : ℕ) (j : Fin n), j.succ.castSucc = j.castSucc.succ
The theorem `Fin.castSucc_fin_succ` states that for all natural numbers `n` and for every element `j` of the finite set `Fin n`, the operation of embedding `j` (incremented by one) into the finite set `Fin (n+1)` is equivalent to first embedding `j` into `Fin (n+1)` and then incrementing it by one. This asserts a kind of commutative property between the `Fin.castSucc` and `Fin.succ` functions.
More concisely: For all natural numbers `n` and elements `j` of `Fin n`, `Fin.castSucc (Fin.succ j) = Fin.succ (Fin.castSucc j)` in `Fin (n+1)`.
|
Fin.val_lt_last
theorem Fin.val_lt_last : ∀ {n : ℕ} {i : Fin (n + 1)}, i ≠ Fin.last n → ↑i < n
This theorem states that for any natural number `n` and any value `i` from the finite set `Fin (n + 1)`, if `i` is not equal to the greatest value of `Fin (n+1)`, represented by `Fin.last n`, then the actual numerical value of `i` (obtained by using the coersion function `↑i`) is strictly less than `n`.
More concisely: For any natural number `n` and `i` in `Fin (n + 1)`, if `i` is not the last element of `Fin (n+1)`, then `↑i` is strictly less than `n`.
|
Fin.is_lt
theorem Fin.is_lt : ∀ {n : ℕ} (a : Fin n), ↑a < n
This theorem, `Fin.is_lt`, states that for any natural number `n` and a finite ordinal `a` of size `n` (represented as `Fin n`), the natural number representation of `a` (obtained by coercing `a` into `ℕ` using `↑a`) is strictly less than `n`. Essentially, it guarantees that any element of a `Fin n` set is less than `n` when viewed as a natural number.
More concisely: For any natural number `n` and finite ordinal `a` of size `n`, the natural number representation of `a` is strictly less than `n`. In Lean notation, `↑a < n`.
|
Fin.eq_last_of_not_lt
theorem Fin.eq_last_of_not_lt : ∀ {n : ℕ} {i : Fin (n + 1)}, ¬↑i < n → i = Fin.last n
This theorem states that for any natural number `n` and any finite number `i` of the form `Fin (n + 1)`, if `i` is not less than `n` when considered as a natural number (notated as `↑i`), then `i` must be equal to the greatest value of `Fin (n+1)`, which is represented by `Fin.last n`. Essentially, this theorem describes a property of the "last" element in a finite set of consecutive numbers starting from zero.
More concisely: For any natural number `n`, the only element `i` of `Fin (n + 1)` with `i ≥ n` is `Fin.last n`.
|
Fin.val_succ
theorem Fin.val_succ : ∀ {n : ℕ} (j : Fin n), ↑j.succ = ↑j + 1
This theorem states that for any natural number `n` and any element `j` of the finite set `Fin n`, the value of the successor of `j` (as defined by the `Fin.succ` function) is equal to the value of `j` incremented by 1. In other words, if we take an element from a finite set of natural numbers up to `n`, apply the `Fin.succ` operation, and then take the value, we will obtain the original value plus one.
More concisely: For any natural number `n` and element `j` of `Fin n`, `Fin.succ j = j + 1`.
|
Fin.val_mk
theorem Fin.val_mk : ∀ {m n : ℕ} (h : m < n), ↑⟨m, h⟩ = m
This theorem, `Fin.val_mk`, states that for any two natural numbers `m` and `n` where `m` is less than `n`, the value of a `Fin n` instance created with `m` as the value and a proof `h` of `m < n` is equal to `m`. In other words, it's ensuring that the `val` field of a `Fin` object correctly reflects the value that was used to construct the object.
More concisely: For all natural numbers `m` and `n` with `m < n`, the value of a `Fin n` instance created with `m` is equal to `m`.
|
Fin.ne_of_lt
theorem Fin.ne_of_lt : ∀ {n : ℕ} {a b : Fin n}, a < b → a ≠ b
This theorem states that for any natural number `n`, and any two elements `a` and `b` from the finite set `Fin n`, if `a` is less than `b`, then `a` and `b` must not be equal. In other words, no number in a finite set of natural numbers can be less than itself, reinforcing the basic property of an ordered set.
More concisely: For all natural numbers n and elements a and b in Fin n, if a < b then a ≠ b.
|
Fin.rev_le_rev
theorem Fin.rev_le_rev : ∀ {n : ℕ} {i j : Fin n}, i.rev ≤ j.rev ↔ j ≤ i
The theorem `Fin.rev_le_rev` states that for all natural numbers `n` and for all elements `i` and `j` of the finite ordered set of size `n`, the reverse of `i` is less than or equal to the reverse of `j` if and only if `j` is less than or equal to `i`. Here, the reverse of an element in the set is defined as `n - 1 - i` for each element `i` in the finite set.
More concisely: For all natural numbers $n$ and elements $i, j$ of a finite set of size $n$, $i < j$ if and only if $(n-1)-i \leq (n-1)-j$.
|
Fin.val_add_one_of_lt
theorem Fin.val_add_one_of_lt : ∀ {n : ℕ} {i : Fin n.succ}, i < Fin.last n → ↑(i + 1) = ↑i + 1
This theorem, `Fin.val_add_one_of_lt`, states that for any natural number `n` and any element `i` of the finite set `Fin (Nat.succ n)`, if `i` is strictly less than the last element of the finite set, then adding one to `i` (using the coercion from `Fin (Nat.succ n)` to `ℕ`) results in the same value as first casting `i` to `ℕ` and then adding one. In other words, for every finite subset of natural numbers augmented by one, if a chosen element doesn't reach the greatest value, incrementing this element leads to the same result whether it's done before or after the type coercion to the natural numbers.
More concisely: For any natural number `n` and `i` in the finite set `Fin (Nat.succ n)`, if `i` is strictly less than the last element of `Fin (Nat.succ n)`, then `(i : ℕ) + 1 = (i + 1 : ℕ)`.
|
Fin.zero_le
theorem Fin.zero_le : ∀ {n : ℕ} (a : Fin (n + 1)), 0 ≤ a
This lean theorem, `Fin.zero_le`, states that for all natural numbers `n` and for any element `a` of the type `Fin (n + 1)`, the number 0 is less than or equal to `a`. In other words, this theorem ensures that no element of the `Fin (n + 1)` type can be less than 0. The `Fin (n + 1)` type in Lean represents a finite set with `n + 1` elements.
More concisely: For all natural numbers `n` and elements `a` in `Fin (n + 1)`, `0 ≤ a`.
|
Fin.castSucc_lt_succ
theorem Fin.castSucc_lt_succ : ∀ {n : ℕ} (i : Fin n), i.castSucc < i.succ
The theorem `Fin.castSucc_lt_succ` states that for any natural number `n` and any element `i` of the type `Fin n` (which is a type representing the finite set of natural numbers less than `n`), the operation of embedding `i` into `Fin (n+1)` via `Fin.castSucc` will always result in a value that is less than the result of the operation `Fin.succ i` (which increments the value of `i` and confirms it's less than or equal to `n`). In other words, if you increment a number and then embed it in the set of natural numbers that are less than `n+1`, that will always be less than if you simply increment the number within the set of natural numbers that are less than `n`.
More concisely: For any natural number `n` and `Fin n` element `i`, `Fin.castSucc i < Fin.succ i`.
|
Fin.rev_rev
theorem Fin.rev_rev : ∀ {n : ℕ} (i : Fin n), i.rev.rev = i
This theorem states that for any natural number `n` and any value `i` of the finite set `Fin n`, applying the `Fin.rev` function twice (i.e., reversing the mapping twice) results in the original value `i`. In other words, the double application of `Fin.rev` is an identity operation on any element of the set `Fin n`.
More concisely: For all natural numbers `n` and elements `i` of `Fin n`, `Fin.rev (Fin.rev i) = i`.
|
Fin.val_one
theorem Fin.val_one : ∀ (n : ℕ), ↑1 = 1
This theorem states that for any natural number `n`, the value of the finite type `Fin` when applied to `1` is equal to `1`. In other words, when we cast `1` as a member of the finite set `Fin n`, where `n` is any natural number, its value remains `1`.
More concisely: For all natural numbers n, the element 1 in the finite type Fin n has the same value as the natural number 1.
|
Fin.succ_last
theorem Fin.succ_last : ∀ (n : ℕ), (Fin.last n).succ = Fin.last n.succ
The theorem `Fin.succ_last` states that for all natural numbers `n`, the successor of the greatest value of `Fin (n+1)` (represented as `Fin.succ (Fin.last n)`) is equal to the greatest value of `Fin (n+2)` (represented as `Fin.last (Nat.succ n)`). In other words, it asserts a property about how the "successor" function (`Fin.succ`) interacts with the "last" function (`Fin.last`), specifically, if you take the successor of the last element in a finite set of size `n+1`, you get the last element in a finite set of size `n+2`.
More concisely: For all natural numbers `n`, `Fin.last (Nat.succ n) = Fin.succ (Fin.last n)`.
|
Fin.cast_succ_eq
theorem Fin.cast_succ_eq : ∀ {n n' : ℕ} (i : Fin n) (h : n.succ = n'.succ), Fin.cast h i.succ = (Fin.cast ⋯ i).succ
This theorem states that for any two natural numbers `n` and `n'` and a `Fin n` element `i`, if the successors of `n` and `n'` are equal (as expressed by `h : n.succ = n'.succ`), then casting the successor of `i` to the `Fin` type constructed with `n'` (i.e., `Fin.cast h i.succ`) is the same as first casting `i` to `Fin n'` and then taking its successor (i.e., `(Fin.cast ⋯ i).succ`). This theorem can be used to rewrite terms in one direction – from left to right. For the reverse direction, you should use `Fin.succ_cast_eq`.
More concisely: For any natural numbers `n`, `n'`, and `Fin n` element `i`, if `n.succ = n'.succ`, then `Fin.cast (n.succ) (i.succ) = (Fin.cast n i).succ`.
|
Fin.castSucc_lt_last
theorem Fin.castSucc_lt_last : ∀ {n : ℕ} (a : Fin n), a.castSucc < Fin.last n
The theorem `Fin.castSucc_lt_last` states that for any natural number `n` and any element `a` of the finite set `Fin n`, the embedding of `a` into the finite set `Fin (n + 1)` using the function `Fin.castSucc` is always less than the greatest value of `Fin (n + 1)`, which is given by the function `Fin.last n`. In other words, if you embed an element from a smaller finite set into a larger one, it will always be less than the maximum value in the larger set.
More concisely: For any natural number `n` and `a` in `Fin n`, `Fin.castSucc a < Fin.last (n + 1)`.
|
Fin.lt_def
theorem Fin.lt_def : ∀ {n : ℕ} {a b : Fin n}, a < b ↔ ↑a < ↑b
This theorem, `Fin.lt_def`, states that for any natural number `n` and any two elements `a` and `b` of the finite set `Fin n`, the statement "a is less than b" is equivalent to the statement "the natural number corresponding to a is less than the natural number corresponding to b". Here, the `↑` operator is used to cast (or "lift") elements of `Fin n` into the natural numbers.
More concisely: For any natural number `n` and `a`, `b` in `Fin n`, `a < b` if and only if `↑a < ↑b`.
|
Fin.last_add_one
theorem Fin.last_add_one : ∀ (n : ℕ), Fin.last n + 1 = 0
This theorem states that for any natural number `n`, if we add `1` to the greatest value of `Fin (n+1)`, we get `0`. In other words, the greatest element of the finite ordered set with `n+1` elements (represented as `Fin (n+1)`), when incremented by `1`, loops back to the smallest element, `0`. This behavior is akin to that of modular arithmetic or circular arrays.
More concisely: The greatest element in `Fin (n+1)` wraps around to `0` when incremented.
|
Fin.succ_ne_zero
theorem Fin.succ_ne_zero : ∀ {n : ℕ} (k : Fin n), k.succ ≠ 0
The theorem `Fin.succ_ne_zero` states that for any natural number `n` and any `k` in the finite set `Fin n`, the successor of `k` in the finite set `Fin (Nat.succ n)` is not zero. In other words, it asserts that when we increment any element in a finite set of natural numbers, the result is never zero. This reflects the fact that there is no wrap-around in the increment operation in the set of natural numbers.
More concisely: For all natural numbers `n` and `k` in `Fin n`, the successor of `k` in `Fin (Nat.succ n)` is non-zero.
|
Fin.lt_iff_val_lt_val
theorem Fin.lt_iff_val_lt_val : ∀ {n : ℕ} {a b : Fin n}, a < b ↔ ↑a < ↑b
This theorem, `Fin.lt_iff_val_lt_val`, states that for any natural number `n` and two finite sequences `a` and `b` with length `n`, `a` is less than `b` if and only if the value of `a` is less than the value of `b`. Here, `↑a` and `↑b` are the coercion of `a` and `b` to natural numbers, respectively. Thus, the comparison is done in terms of the respective natural number values of `a` and `b`.
More concisely: For any finite sequences `a` and `b` of natural numbers of length `n`, `a` is less than `b` if and only if the natural numbers `↑a` and `↑b` satisfy `↑a < ↑b`.
|
Fin.rev_castSucc
theorem Fin.rev_castSucc : ∀ {n : ℕ} (k : Fin n), k.castSucc.rev = k.rev.succ
The theorem `Fin.rev_castSucc` states that for all natural numbers `n` and for all elements `k` of type `Fin n`, the operation of reversing the order of elements (`Fin.rev`) after embedding `k` into a larger finite set (`Fin.castSucc k`) is equivalent to the operation of first reversing the order of elements and then incrementing the resulting element (`Fin.succ (Fin.rev k)`). Essentially, this theorem is about the equivalence of two composite operations on elements of finite sets in Lean 4.
More concisely: For all natural numbers `n` and elements `k` of `Fin n`, `Fin.rev (Fin.castSucc k)` is equivalent to `Fin.succ (Fin.rev k)`.
|
Fin.eta
theorem Fin.eta : ∀ {n : ℕ} (a : Fin n) (h : ↑a < n), ⟨↑a, h⟩ = a
This theorem, `Fin.eta`, states that for any natural number `n` and any `a` which is an element of the "Fin" type (a type that represents a finite set of size `n`), if the value of `a` (`↑a`) is less than `n` (denoted by `h`), then creating a new "Fin" object with the same value and the condition `h` will yield the same "Fin" object `a`. In other words, for elements in the finite set, you can't have two distinct elements with the same value.
More concisely: For any natural number `n` and element `a` of the finite type `Fin n`, if `a` has value less than `n`, then `Fin.mk (a : nat) (h : a < n)` equals `a`.
|
Fin.forall_fin_two
theorem Fin.forall_fin_two : ∀ {p : Fin 2 → Prop}, (∀ (i : Fin 2), p i) ↔ p 0 ∧ p 1
This theorem, `Fin.forall_fin_two`, states that for any property `p` applicable to elements of the set `Fin 2` (which contains two elements represented as `0` and `1`), the property `p` holds for all elements of the `Fin 2` set if and only if the property `p` holds for `0` and the property `p` holds for `1`. In other words, if you can prove that `p` is true for both `0` and `1`, then you can assert that `p` is true for any element in `Fin 2`, and vice versa.
More concisely: For any property `p`, `p` holds for all elements of `Fin 2` if and only if `p` holds for both `0` and `1` in `Fin 2`.
|
Fin.le_castSucc_iff
theorem Fin.le_castSucc_iff : ∀ {n : ℕ} {i : Fin (n + 1)} {j : Fin n}, i ≤ j.castSucc ↔ i < j.succ
The theorem `Fin.le_castSucc_iff` states that for any natural number `n` and any two finite ordinals `i` and `j` such that `i` belongs to `Fin (n + 1)` and `j` belongs to `Fin n`, `i` is less than or equal to the embedding of `j` into `Fin (n + 1)` using `castSucc` if and only if `i` is less than the successor of `j` in `Fin (n + 1)`. This theorem provides a way to compare elements in different finite ordinal types, linking the relation of being less than or equal to under embedding and being less than under successorship.
More concisely: For any natural number `n`, `Fin.le_castSucc_iff` asserts that `i ≤ castSucc i'` in `Fin (n + 1)` if and only if `i < succ i'` holds in `Fin n`, where `i` is an element of `Fin (n + 1)` and `i'` is an element of `Fin n`.
|
Fin.succ_pred
theorem Fin.succ_pred : ∀ {n : ℕ} (i : Fin (n + 1)) (h : i ≠ 0), (i.pred h).succ = i
The theorem `Fin.succ_pred` asserts that for any natural number `n` and any nonzero element `i` of `Fin (n + 1)`, the successor of the predecessor of `i` is `i` itself. This theorem reflects that the operations `Fin.succ` and `Fin.pred` are inverses of each other for nonzero elements in the finite set `Fin (n + 1)`. In other words, if you take a nonzero element `i` from the set `Fin (n+1)`, compute its predecessor, and then compute the successor of the result, you end up with the original element `i`.
More concisely: For any natural number `n` and nonzero `i` in `Fin (n + 1)`, `Fin.pred (Fin.pred i) = i`.
|
Fin.val_zero
theorem Fin.val_zero : ∀ (n : ℕ), ↑0 = 0
This theorem, named `Fin.val_zero`, states that for any natural number `n`, the value of the zero element in the finite set of size `n` is equal to zero. In other words, when you coerce zero from the finite set to the natural numbers, you get zero.
More concisely: For any natural number `n`, the zero element of the finite set of size `n` equals the natural number zero.
|
Fin.size_pos
theorem Fin.size_pos : ∀ {n : ℕ}, Fin n → 0 < n
This theorem, `Fin.size_pos`, states that for all natural numbers `n`, if there exists an element in the finite set `Fin n`, then `n` must always be greater than 0. The finite set `Fin n` represents a set of `n` distinct elements, so if there exists an element in this set, it implies that the set is not empty, consequently `n` is positive.
More concisely: If a finite set of size `n` is non-empty, then `n` is a positive natural number.
|
Fin.mk_zero
theorem Fin.mk_zero : ∀ {n : ℕ}, ⟨0, ⋯⟩ = 0
This theorem states that for all natural numbers `n`, the finite type `Fin n` when created with `val` as `0` and some proof `isLt` is equal to `0`. In other words, the zero element of any finite type of size `n` is effectively the same as the natural number zero. This is a feature of the way finite types are defined in Lean.
More concisely: For all natural numbers `n`, the zero element of the finite type `Fin n` is equal to the natural number zero.
|
Fin.coeSucc_eq_succ
theorem Fin.coeSucc_eq_succ : ∀ {n : ℕ} {a : Fin n}, a.castSucc + 1 = a.succ
The theorem `Fin.coeSucc_eq_succ` states that for all natural numbers `n` and for all elements `a` of the finite set `Fin n`, the sum of the element `a` embedded into the finite set `Fin (n+1)` (performed by `Fin.castSucc a`) and `1` is equal to the successor of the element `a` in the finite set `Fin (Nat.succ n)` (performed by `Fin.succ a`). In other words, embedding `a` into a larger finite set and incrementing it yields the same result as directly getting the successor of `a` in its finite set.
More concisely: For all natural numbers `n` and elements `a` in `Fin n`, `Fin.castSucc a + 1 = Fin.succ a` in `Fin (Nat.succ n)`.
|
Fin.pred_succ
theorem Fin.pred_succ : ∀ {n : ℕ} (i : Fin n) {h : i.succ ≠ 0}, i.succ.pred h = i
The theorem `Fin.pred_succ` states that for every natural number `n` and every `i` in `Fin n`, when the successor of `i` is not zero, its predecessor is `i` itself. This essentially formalizes a property about how incrementing (`Fin.succ`) and decrementing (`Fin.pred`) interact in the context of the type `Fin n`, which represents the set `{0, 1, ..., n-1}`.
More concisely: For all natural numbers `n` and `i` in `Fin n` with `Fin.succ i ≠ 0`, `Fin.pred (Fin.succ i) = i`.
|
Fin.val_rev
theorem Fin.val_rev : ∀ {n : ℕ} (i : Fin n), ↑i.rev = n - (↑i + 1)
This theorem, `Fin.val_rev`, states that for any natural number `n` and any element `i` of the type `Fin n`, the numerical value of the reversed version of `i` (obtained through the function `Fin.rev`) is equal to `n` minus the numerical value of `i` minus one. In other words, the function `Fin.rev` flips the order of the set `{0, 1, ..., n-1}` by mapping each number `i` to `n - i - 1`.
More concisely: For any natural number `n` and element `i` of finite type `Fin n`, the value of `i` in the reversed finite sequence `Fin.rev` equals `n - i - 1`.
|
Fin.rev_succ
theorem Fin.rev_succ : ∀ {n : ℕ} (k : Fin n), k.succ.rev = k.rev.castSucc
The theorem `Fin.rev_succ` states that for all natural numbers `n` and for any `k` of type `Fin n` (which is a finite ordered list of length `n`), the reverse of the successively next element of `k` is equivalent to the casting of the reverse of `k` into a list of one longer length. In other words, first incrementing `k` and then reversing equals to first reversing `k` and then casting it into a list of length `n+1`.
More concisely: For any finite list `k` of length `n` in `Fin`, the reversed successor of `k` is equivalent to appending `0` to the reversed list of length `n+1` obtained from `k`.
|
Fin.succ_zero_eq_one
theorem Fin.succ_zero_eq_one : ∀ {n : ℕ}, Fin.succ 0 = 1
This theorem, named `Fin.succ_zero_eq_one`, states that for any natural number `n`, the successor of `0` in the finite sequence of size `n` (denoted as `Fin.succ 0`) is equal to `1`. In simpler terms, it implies that if you increment `0` in the series of the first `n` natural numbers (including zero), you will always get `1`.
More concisely: For any natural number `n`, `Fin.succ 0` equals `1` in the finite sequence of length `n+1`.
|
Fin.succ_one_eq_two
theorem Fin.succ_one_eq_two : ∀ {n : ℕ}, Fin.succ 1 = 2
This theorem, `Fin.succ_one_eq_two`, states that for all natural numbers `n`, the successor of 1 in the finite set `Fin n` is always 2. In other words, when you apply the `Fin.succ` function to 1, the result is always 2, regardless of the size of the finite set you are working within. This theorem is intended to be used by the `dsimp` tactic in Lean 4, which simplifies expressions.
More concisely: For all natural numbers n, Fin.succ (1 : Fin n) = 2 : Fin n.
or more mathematically,
The successor of 1 in the finite set Fin n is always equal to the number 2.
|
Fin.addNat_cast
theorem Fin.addNat_cast : ∀ {n n' m : ℕ} (i : Fin n') (h : n' = n), (Fin.cast h i).addNat m = Fin.cast ⋯ (i.addNat m)
The theorem `Fin.addNat_cast` states that for any natural numbers `n`, `n'`, and `m`, and any element `i` of the finite set corresponding to `n'`, if `n'` is equal to `n`, then adding `m` to `i` after casting it to the finite set corresponding to `n` is the same as adding `m` to `i` first, then casting the result to the finite set corresponding to `n + m`. This theorem is particularly useful for rewriting expressions in the forward direction. For rewriting in the reverse direction, refer to `Fin.cast_addNat_left`.
More concisely: For any natural numbers `n`, `n'`, `m`, and element `i` of the finite set `Fin n'`, if `n' = n` then adding `m` to `i` in the finite set `Fin (n + m)` is equivalent to adding `m` to `i` in `Fin n` and then casting the result to `Fin (n + m)`.
|
Fin.succ_pos
theorem Fin.succ_pos : ∀ {n : ℕ} (a : Fin n), 0 < a.succ
The theorem `Fin.succ_pos` states that for all natural numbers `n` and for every element `a` of the finite set `Fin n`, the successor of `a` is greater than zero. Here, `Fin n` represents the set of natural numbers less than `n`, and `Fin.succ` is a function that takes an element from `Fin n` and returns an element in `Fin (n+1)`. The idea is that the successor function always produces a positive result because it increases the input by 1.
More concisely: For all natural numbers `n` and elements `a` in `Fin n`, `Fin.succ a` is a positive natural number.
|
Fin.rev_last
theorem Fin.rev_last : ∀ (n : ℕ), (Fin.last n).rev = 0
This theorem states that for any natural number `n`, if you reverse `Fin.last n`, you get `0`. `Fin.last n` refers to the greatest value of `Fin (n+1)`, and `Fin.rev` is a function that maps `0` to `n-1`, `1` to `n-2`, ..., `n-1` to `0`. Therefore, if the greatest value of `Fin(n+1)` is reversed, it gives `0`.
More concisely: For any natural number `n`, the greatest element in `Fin (n+1)` is equal to `0` when reversed using the `Fin.rev` function.
|