Fin.rightInverse_cast
theorem Fin.rightInverse_cast : ∀ {n m : ℕ} (eq : n = m), Function.RightInverse (Fin.cast ⋯) (Fin.cast eq)
The theorem `Fin.rightInverse_cast` states that for all natural numbers `n` and `m`, given an equality `eq` between `n` and `m`, the function `Fin.cast` with an unspecified equality is a right inverse to the function `Fin.cast eq`. In other words, if we apply `Fin.cast eq` and then apply `Fin.cast` with some equality, we get back to the original element. This is equivalent to saying that the composition of these two functions is the identity function.
More concisely: For all natural numbers `n` and `m` and equality `eq` between them, `Fin.cast eq` and `Fin.cast` composition is equal to the identity function on `n`.
|
Fin.size_positive
theorem Fin.size_positive : ∀ {n : ℕ}, Fin n → 0 < n
This theorem states that if you have an element of the finite set `Fin n`, then `n` is always greater than zero. In other words, if an element exists in this set, it implies that the size of the set (represented by `n`) must be positive. The `Fin` type in Lean represents a finite set of natural numbers from 0 to `n-1`, therefore it is only possible to have an element of `Fin n` if `n` is greater than zero.
More concisely: If $x$ is an element of the finite set `Fin n`, then $n > 0$.
|
Fin.castPred_castSucc
theorem Fin.castPred_castSucc :
∀ {n : ℕ} {i : Fin n} (h' : optParam (i.castSucc ≠ Fin.last n) ⋯), i.castSucc.castPred h' = i
The theorem `Fin.castPred_castSucc` states that for any natural number `n` and for any `i : Fin n`, provided the optional parameter `h'` which assures that the successor of `i` when casted to `Fin (n + 1)` is not the greatest value of `Fin (n+1)`, casting the successor of `i` to `Fin (n + 1)` and then casting it back to `Fin n` (given that it is not the greatest value of `Fin (n+1)`), you end up with the original `i`. In other words, the operations of casting to successor and then casting to predecessor are inverses of each other under the condition that the value is not the greatest value in `Fin (n+1)`.
More concisely: For any natural number `n` and `i : Fin n`, if `i + 1` is not the maximum value of `Fin (n + 1)`, then `Fin.castPred (Fin.castSucc i) = i`.
|
Fin.val_fin_lt
theorem Fin.val_fin_lt : ∀ {n : ℕ} {a b : Fin n}, ↑a < ↑b ↔ a < b
This theorem states that, given two natural numbers `a` and `b` within the range of a finite set `Fin n`, the inequality `a < b` holds if and only if `a < b` also holds when `a` and `b` are considered as elements of `Fin n`. In other words, the 'less than' relation between `a` and `b` is preserved when transitioning between the natural numbers and `Fin n`.
More concisely: The theorem asserts that the relation `a < b` holds for natural numbers `a` and `b` in the finite set `Fin n` if and only if it holds for their corresponding elements in `Fin n`.
|
Fin.prop
theorem Fin.prop : ∀ {n : ℕ} (a : Fin n), ↑a < n
This theorem, `Fin.prop`, states that for any natural number `n` and any element `a` of the finite sequence of length `n` (denoted as `Fin n`), the value of `a` when cast to a natural number (i.e., `↑a`) is less than `n`. Essentially, it formalizes the idea that an element of a finite sequence is always less than the length of that sequence.
More concisely: For any natural number `n` and element `a` in the finite sequence `Fin n`, the natural number `↑a` (the coercion of `a` to a natural number) is less than `n`.
|
Fin.val_injective
theorem Fin.val_injective : ∀ {n : ℕ}, Function.Injective Fin.val
The theorem `Fin.val_injective` states that for any natural number `n`, the function `Fin.val` is injective. The function `Fin.val` maps an instance of the finite type `Fin n` to natural numbers. Being injective means that if `Fin.val` applied to two instances of `Fin n` yields the same natural number, then those two instances must be identical. In other words, no two different elements of `Fin n` are mapped to the same natural number by `Fin.val`.
More concisely: For any natural numbers `m` and `n`, if `Fin.val m = Fin.val n` then `m = n`. (Here, `Fin.val m` and `Fin.val n` denote the natural numbers associated with the finite types `Fin m` and `Fin n`, respectively.)
|
Fin.coe_orderIso_apply
theorem Fin.coe_orderIso_apply : ∀ {n m : ℕ} (e : Fin n ≃o Fin m) (i : Fin n), ↑(e i) = ↑i
This theorem states that if `e` is an order isomorphism between the finite ordered sets `Fin n` and `Fin m`, then the size of the sets `n` and `m` must be equal, and `e` is the identity map. More specifically, for each element `i` from `Fin n`, the natural number value of applying the isomorphism `e` to `i` is equal to the natural number value of `i` itself.
More concisely: If `e` is an order isomorphism between finite ordered sets `Fin n` and `Fin m`, then `n = m` and `e` is the identity map on both sets.
|
Fin.castSucc_pred_eq_pred_castSucc
theorem Fin.castSucc_pred_eq_pred_castSucc :
∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ 0) (ha' : optParam (a.castSucc ≠ 0) ⋯),
(a.pred ha).castSucc = a.castSucc.pred ha'
This theorem, `Fin.castSucc_pred_eq_pred_castSucc`, states that for any natural number `n` and any `a` which is a non-zero element of `Fin (n + 1)`, the operation of first taking the predecessor of `a` and then embedding the result in `Fin (n + 2)` using `Fin.castSucc` is equivalent to the operation of first embedding `a` in `Fin (n + 2)` using `Fin.castSucc` and then taking its predecessor. The second argument of the `Fin.pred` function is a proof that the input is non-zero, and in this case these proofs are represented by `ha` for `a` and `ha'` for `Fin.castSucc a`. The `optParam` is used to provide a default proof for `ha'` in case it is not supplied.
More concisely: For any natural number `n` and non-zero `a` in `Fin (n + 1)`, `Fin.pred (Fin.castSucc a)` is equivalent to `Fin.castSucc (Fin.pred a)`.
|
Fin.pos_iff_ne_zero'
theorem Fin.pos_iff_ne_zero' : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), 0 < a ↔ a ≠ 0
This theorem, `Fin.pos_iff_ne_zero'`, states that for any natural number `n` that is not zero (`NeZero n`) and a finite ordinal `a` of `n` (`Fin n`), `a` is greater than zero if and only if `a` is not equal to zero. Unlike `Fin.pos_iff_ne_zero` in `Std`, which only applies to `Fin (n+1)`, this theorem applies to any non-zero `n`.
More concisely: For any natural number `n` and finite ordinal `a` of `n`, `a` is greater than zero if and only if `a` is not equal to the zero ordinal of type `Fin n`.
|
Fin.strictMono_unique
theorem Fin.strictMono_unique :
∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f g : Fin n → α},
StrictMono f → StrictMono g → Set.range f = Set.range g → f = g
This theorem states that for any natural number `n` and any type `α` that has a preorder structure, if `f` and `g` are two strictly monotone functions from `Fin n` (the type of finite ordinals less than `n`) to `α`, and if the ranges of `f` and `g` are equal, then `f` and `g` must be the same function. In other words, two strictly increasing functions from a finite ordinal set to a preordered set are uniquely determined by their range.
More concisely: Given any natural number `n` and a preordered type `α`, if `f` and `g` are strictly monotone functions from `Fin n` to `α` with equal ranges, then `f` equals `g`.
|
Fin.succ_injective
theorem Fin.succ_injective : ∀ (n : ℕ), Function.Injective Fin.succ
This theorem states that, for every natural number `n`, the `Fin.succ` function is injective. In other words, if `Fin.succ` is applied to two distinct values of the type `Fin n`, it will yield two distinct values of the type `Fin (Nat.succ n)`. In mathematical terms, if we have `Fin.succ x = Fin.succ y`, it necessarily follows that `x = y`.
More concisely: For every natural number `n`, the function `Fin.succ : Fin n -> Fin (Nat.succ n)` is an injection.
|
Fin.coe_eq_castSucc
theorem Fin.coe_eq_castSucc : ∀ {n : ℕ} {a : Fin n}, ↑↑a = a.castSucc
The theorem `Fin.coe_eq_castSucc` states that for any natural number `n` and any element `a` of the finite set `Fin n`, converting `a` to a natural number and then embedding it back into `Fin (n+1)` (i.e., `↑↑a`) is equivalent to directly embedding `a` into `Fin (n+1)` using the `Fin.castSucc` function. In other words, it asserts the equivalence of two ways of embedding an element of `Fin n` into `Fin (n+1)`.
More concisely: For any natural number `n` and element `a` of `Fin n`, `↑↑a` equals `Fin.castSucc a` in `Fin (n+1)`.
|
Fin.bot_eq_zero
theorem Fin.bot_eq_zero : ∀ (n : ℕ), ⊥ = 0
This theorem states that for any natural number `n`, the bottom element of the finite set `Fin n` is equal to zero. This is a fundamental property of the `Fin` data type in Lean, which is a type used to represent a finite set of natural numbers less than some fixed natural number `n`.
More concisely: For any natural number $n$, the bottom element of the finite set $Fin(n)$ is equal to $0$.
|
Fin.cast_val_eq_self
theorem Fin.cast_val_eq_self : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), ↑↑a = a
This theorem states that for any non-zero natural number `n`, if you have a value `a` that is of type `Fin n` (which represents a finite set of `n` distinct elements), then converting `a` twice into `Fin n` type will result in the original value `a`. Essentially, it asserts that double conversion of a `Fin n` value to `Fin n` doesn't change the value.
More concisely: For any non-zero natural number `n` and any `a` of type `Fin n`, converting `a` to `Fin n` twice equals `a`. In Lean syntax, `(Fin.coe : Fin n → nat) (Fin.coe a) = a`.
|
Fin.modNat.proof_1
theorem Fin.modNat.proof_1 : ∀ {n m : ℕ} (i : Fin (m * n)), ↑i % n < n
This theorem states that for any two natural numbers `n` and `m`, and any finite number `i` in the interval from 0 to `m * n`, the remainder of `i` when divided by `n` is always less than `n`. This corresponds to the general property of the modulo operation (`%`), which guarantees that the result is always in the range `[0, n)` for positive `n`.
More concisely: For all natural numbers n and m, and all finite i in the range 0 <= i < m * n, the remainder i % n < n holds.
|
Fin.zero_le'
theorem Fin.zero_le' : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), 0 ≤ a
The theorem `Fin.zero_le'` states that for any natural number `n` that is not zero, and any element `a` of the finite ordered set `Fin n`, 0 is less than or equal to `a`. This is a more general version of the `Fin.zero_le` theorem in the `Std` library, which only applies when `n` is incremented by 1 (`Fin (n+1)`). The current theorem instead leverages a `NeZero n` typeclass hypothesis.
More concisely: For any natural number `n` and any element `a` in the finite ordered set `Fin n` with `n ≠ 0`, `0 ≤ a`.
|
Fin.cast_nat_eq_last
theorem Fin.cast_nat_eq_last : ∀ (n : ℕ), ↑n = Fin.last n
This theorem states that for all natural numbers `n`, the canonical embedding of `n` to the type `Fin (n+1)` is equal to the greatest value in `Fin (n+1)`. In other words, when we cast a natural number `n` to the type `Fin (n+1)`, we get the last, or maximum, element in the finite ordered set `Fin (n+1)`. This ordered set contains `n + 1` elements indexed from `0` to `n`.
More concisely: The canonical embedding of a natural number `n` into `Fin (n+1)` is the greatest element in `Fin (n+1)`.
|
Fin.castIso_to_equiv
theorem Fin.castIso_to_equiv : ∀ {n m : ℕ} (h : n = m), (Fin.castIso h).toEquiv = Equiv.cast ⋯
The theorem `Fin.castIso_to_equiv` states that for any two natural numbers `n` and `m` which are equal (i.e., `h : n = m`), the equivalence obtained by considering `Fin.castIso h` (which embeds `n` into an equal `Fin` type and is generally preferred) and taking its `toEquiv` function is the same as the equivalence obtained using `Equiv.cast`. In other words, although `Fin.castIso` is usually better, there are certain cases where we might want to use the more generic `cast` operation, and this theorem ensures that the two approaches are equivalent in those cases.
More concisely: For any equal natural numbers `n` and `m`, the equivalences obtained using `Fin.castIso h toEquiv` and `Equiv.cast` are equal.
|
Fin.heq_fun₂_iff
theorem Fin.heq_fun₂_iff :
∀ {α : Sort u_1} {k l k' l' : ℕ} (h : k = l) (h' : k' = l') {f : Fin k → Fin k' → α} {g : Fin l → Fin l' → α},
HEq f g ↔ ∀ (i : Fin k) (j : Fin k'), f i j = g ⟨↑i, ⋯⟩ ⟨↑j, ⋯⟩
This theorem states that for any type `α`, given natural numbers `k`, `l`, `k'`, and `l'`, if `k = l` and `k' = l'`, then for any two functions `f : Fin k → Fin k' → α` and `g : Fin l → Fin l' → α`, these two functions are identical (in the sense of heterogeneous equality `HEq`) if and only if they produce the same output for every pair of inputs drawn from the finite sets `Fin k` and `Fin k'`. Here, `Fin n` refers to the set of natural numbers less than `n`.
More concisely: For any types `α` and natural numbers `k`, `l`, `k'`, `l'`, if `k = l`, `k' = l'`, and for all `i < k` and `j < k'`, `f i j = g i j`, then `f = g` (heterogeneously).
|
Fin.succ_castPred_eq_castPred_succ
theorem Fin.succ_castPred_eq_castPred_succ :
∀ {n : ℕ} {a : Fin (n + 1)} (ha : a ≠ Fin.last n) (ha' : optParam (a.succ ≠ Fin.last (n + 1)) ⋯),
(a.castPred ha).succ = a.succ.castPred ha'
The theorem `Fin.succ_castPred_eq_castPred_succ` states that for any natural number `n` and any element `a` of the type `Fin (n + 1)`, given that `a` is not the last element of `Fin n` (i.e., `a ≠ Fin.last n`) and optionally assuming that the successor of `a` is not the last element of `Fin (n + 1)`, the successor of the element obtained by casting `a` to `Fin n` (i.e., `Fin.succ (Fin.castPred a ha)`) is equal to the result of casting the successor of `a` to `Fin n` (i.e., `Fin.castPred (Fin.succ a) ha'`). In other words, this theorem ensures the commutativity of the `Fin.succ` and `Fin.castPred` operations in the finite sequence `Fin` under certain conditions.
More concisely: For any natural number `n` and elements `a` in `Fin (n + 1)` not equal to the last element of `Fin n`, the successor of `Fin.castPred a` is equal to `Fin.castPred (Fin.succ a)`.
|
Fin.castSucc_eq_zero_iff'
theorem Fin.castSucc_eq_zero_iff' : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), a.castSucc = 0 ↔ a = 0
This theorem, `Fin.castSucc_eq_zero_iff'`, states that for any natural number `n` that is not zero (guaranteed by the `NeZero n` typeclass hypothesis) and for any `a` which is an element of `Fin n`, `a.castSucc` being equal to zero is equivalent to `a` being zero. Essentially, it asserts that incrementing a finite number `a` in the set `Fin n` results in zero if and only if `a` is zero. This theorem provides a more general version of the `Fin.castSucc_eq_zero_iff` theorem from the `Std` library, which only applies when `n` is specifically `n+1`.
More concisely: For any natural number `n` and `a` in `Fin n`, `a.castSucc` equals zero if and only if `a` is zero.
|
Fin.succ_ne_last_iff
theorem Fin.succ_ne_last_iff : ∀ {n : ℕ} (a : Fin (n + 1)), a.succ ≠ Fin.last (n + 1) ↔ a ≠ Fin.last n
This theorem, `Fin.succ_ne_last_iff`, states that for any natural number `n` and a finite ordinal `a` of `n+1`, the successor of `a` is not equal to the greatest value of `Fin (n+1)` if and only if `a` is not equal to the greatest value of `Fin n`. In other words, incrementing a finite ordinal does not result in the maximum finite ordinal of the next type if and only if the original finite ordinal was not the maximum of its type.
More concisely: The successor of a finite ordinal is not the maximum value of the next type if and only if the ordinal is not the maximum value of its type.
|
Fin.le_iff_val_le_val
theorem Fin.le_iff_val_le_val : ∀ {n : ℕ} {a b : Fin n}, a ≤ b ↔ ↑a ≤ ↑b
This theorem states that for any two elements `a` and `b` of the set `Fin n` (which represents a finite subset of natural numbers with `n` elements), `a` is less than or equal to `b` if and only if the value of `a` (denoted by `↑a`) is less than or equal to the value of `b` (denoted by `↑b`). In other words, the order relation in `Fin n` is the same as the order relation in the natural numbers, as reflected by their values.
More concisely: For any `a, b` in `Fin n`, `a ≤ b` if and only if `↑a ≤ ↑b` in the natural numbers.
|
Fin.strictMono_castLE
theorem Fin.strictMono_castLE : ∀ {n m : ℕ} (h : n ≤ m), StrictMono (Fin.castLE h)
The theorem `Fin.strictMono_castLE` states that for any two natural numbers `n` and `m`, where `n` is less than or equal to `m`, the function `Fin.castLE h` is strictly monotone. This means that if we have two elements in `Fin n`, say `a` and `b`, where `a` is less than `b`, then `Fin.castLE h a` is less than `Fin.castLE h b` when these elements are embedded into the larger `Fin m` type. In essence, the `Fin.castLE` function preserves the ordering of elements when casting from a smaller `Fin` type to a larger one.
More concisely: For all natural numbers `n` and `m` with `n <= m`, the function `Fin.castLE : Fin n -> Fin m` is strictly monotone, meaning that `Fin.castLE a < Fin.castLE b` for all `a < b` in `Fin n`.
|
Fin.coe_fin_one
theorem Fin.coe_fin_one : ∀ (a : Fin 1), ↑a = 0
This theorem states that for any element `a` of the type `Fin 1`, the coersion of `a` to its corresponding natural number is always 0. In other words, any element of `Fin 1` maps to the natural number 0 when coersed. This is because `Fin 1` has only one element, 0, in its set.
More concisely: For any element `a` in `Fin 1`, its coercion to the natural numbers is the constant 0. (Or equivalently, the unique element of `Fin 1` is mapped to the natural number 0 during coercion.)
|
Fin.antitone_iff_succ_le
theorem Fin.antitone_iff_succ_le :
∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
Antitone f ↔ ∀ (i : Fin n), f i.succ ≤ f i.castSucc
The theorem `Fin.antitone_iff_succ_le` states that for a function `f` mapping from the finite ordered set of size `n + 1` to any preordered set `α`, the function is antitone (that is, it preserves the order inversely: if `a ≤ b` then `f(b) ≤ f(a)`) if and only if the value of `f` at `i + 1` is less than or equal to the value of `f` at `i` for all `i` in the finite ordered set of size `n`. In other words, this theorem characterizes antitone functions on finite ordered sets in terms of the inequality `f(i + 1) ≤ f(i)`.
More concisely: A function from a finite ordered set to a preordered set is antitone if and only if the successor application of the function is order-preserving, that is, `f(i + 1) ≤ f(i)` for all `i` in the finite ordered set.
|
Fin.castSucc_castPred
theorem Fin.castSucc_castPred : ∀ {n : ℕ} (i : Fin (n + 1)) (h : i ≠ Fin.last n), (i.castPred h).castSucc = i := by
sorry
The theorem `Fin.castSucc_castPred` states that for any natural number `n` and an element `i` of `Fin (n + 1)` which is not the last element of `Fin (n + 1)`, embedding `i` back into `Fin (n + 1)` after casting it to `Fin n` returns the original element `i`. This means that the casting operations `castPred` and `castSucc` are inverses to each other when excluding the last element of `Fin (n + 1)`.
More concisely: For all natural numbers `n` and elements `i` of `Fin (n + 1)` that are not the last element, `castPred (castSucc i) = i` holds in `Fin (n + 1)`.
|
Fin.castSucc_ne_zero_iff'
theorem Fin.castSucc_ne_zero_iff' : ∀ {n : ℕ} [inst : NeZero n] (a : Fin n), a.castSucc ≠ 0 ↔ a ≠ 0
This theorem, `Fin.castSucc_ne_zero_iff'`, states that for all natural numbers `n` (where `n` is not zero, as indicated by the `NeZero n` typeclass), and for any `a` in `Fin n`, `a.castSucc` being not equal to zero is equivalent to `a` being not equal to zero. In other words, it provides a condition to check whether an element of `Fin n` is not zero, after casting it to `Fin (n+1)` using the `castSucc` operation. This is more general than `Fin.castSucc_ne_zero_iff` in `Std`, which only applies when `n` is specifically `n+1`.
More concisely: For any natural number `n` and element `a` in `Fin n` (non-zero), `a.castSucc ≠ 0` if and only if `a ≠ 0`.
|
Fin.monotone_iff_le_succ
theorem Fin.monotone_iff_le_succ :
∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
Monotone f ↔ ∀ (i : Fin n), f i.castSucc ≤ f i.succ
The theorem `Fin.monotone_iff_le_succ` states that for any natural number `n` and for any type `α` that has a preorder, a function `f` from `Fin(n+1)` to `α` is monotone if and only if for all `i` of type `Fin n`, `f(i)` is less than or equal to `f(i + 1)`. Here, `Fin(n+1)` and `Fin n` are types representing finite sets of `n+1` and `n` natural numbers, respectively. The functions `Fin.castSucc` and `Fin.succ` are used to embed `i : Fin n` in `Fin (n+1)` and to increment a value in `Fin n`, respectively.
More concisely: A function from the finite set of natural numbers up to n+1 to a preordered type is monotone if and only if its restriction to the finite set of natural numbers up to n satisfies i ≤ i' implies f i ≤ f i'.
|
Fin.castSucc_zero'
theorem Fin.castSucc_zero' : ∀ {n : ℕ} [inst : NeZero n], Fin.castSucc 0 = 0
The theorem `Fin.castSucc_zero'` states that for any non-zero natural number `n`, the function `Fin.castSucc`, when applied to `0`, results in `0`. This is different from the `Fin.castSucc_zero` in the standard library, which only applies when `n` is incremented by `1`. This version of the theorem instead utilizes a typeclass hypothesis `NeZero n`, which ensures that `n` is non-zero.
More concisely: For any non-zero natural number `n`, `Fin.castSucc 0 = 0`.
|
Fin.castSucc_pos'
theorem Fin.castSucc_pos' : ∀ {n : ℕ} [inst : NeZero n] {i : Fin n}, 0 < i → 0 < i.castSucc
The theorem `Fin.castSucc_pos'` states that for any natural number `n` that is not zero, and any element `i` of the finite set `Fin n`, if `i` is greater than zero, then the "successor" of `i` (obtained through the function `castSucc`) is also greater than zero. This theorem is a generalized form of the `Fin.castSucc_pos` in `Std`, which is only applicable in `Fin (n+1)`, but this one uses the `NeZero n` typeclass to ensure that `n` is not zero.
More concisely: For any natural number `n` with `n ≠ 0` and any `i ∈ Fin n` with `i ≠ 0`, the successor of `i` in `Fin n` is also a non-zero element.
|
Fin.cast_eq_cast
theorem Fin.cast_eq_cast : ∀ {n m : ℕ} (h : n = m), Fin.cast h = cast ⋯
This theorem, `Fin.cast_eq_cast`, states that for any two natural numbers `n` and `m`, given a proof `h` that `n` equals `m`, the function `Fin.cast h` is equivalent to the generic `cast` function. This theorem highlights that even though it's often advantageous to use `Fin.cast`, it might be beneficial to use the more generic `cast` function in certain cases when applying a generic theorem about `cast`.
More concisely: For any natural numbers `n` and `m` and proof `h` that `n = m`, `Fin.cast h` is equivalent to the `cast` function applied to `h`.
|
Fin.le_zero_iff'
theorem Fin.le_zero_iff' : ∀ {n : ℕ} [inst : NeZero n] {k : Fin n}, k ≤ 0 ↔ k = 0
This theorem, `Fin.le_zero_iff'`, establishes a condition for a certain non-zero natural number `k` of a finite set `Fin n` to be less than or equal to zero. In the standard library, the `Fin.le_zero_iff` applies only to `Fin (n+1)`. However, this theorem extends that to include a `NeZero n` typeclass hypothesis, thus making it applicable to a wider range of cases. The theorem states that for all non-zero natural numbers `n` and any `k` within `Fin n`, `k` is less than or equal to zero if and only if `k` is equal to zero.
More concisely: For any finite set `Fin n` and non-zero natural number `n`, the natural number `k` in `Fin n` is less than or equal to zero if and only if `k` is equal to the zero element of `Fin n`.
|
Mathlib.Data.Fin.Basic._auxLemma.11
theorem Mathlib.Data.Fin.Basic._auxLemma.11 : ∀ {n : ℕ} {a b : Fin n}, (a = b) = (↑a = ↑b)
This theorem, `Mathlib.Data.Fin.Basic._auxLemma.11`, states that for any natural number `n` and any two elements `a` and `b` of the finite set of size `n` (denoted as `Fin n` in Lean), the equality of `a` and `b` is equivalent to the equality of their respective "coerced" or "promoted" values. In Lean, the `↑` symbol is used to denote the coercion of a term from one type to another, so `↑a` and `↑b` are the natural number representations of `a` and `b` respectively.
More concisely: For any natural number `n` and elements `a` and `b` in `Fin n`, the equality of `a` and `b` is equivalent to the equality of their coerced natural number representations, i.e., `↑a = ↑b`.
|
Fin.succ_one_eq_two'
theorem Fin.succ_one_eq_two' : ∀ {n : ℕ} [inst : NeZero n], Fin.succ 1 = 2
The theorem `Fin.succ_one_eq_two'` states that for any natural number `n` that is not zero, the successor of 1 in the finite sequence of length `n` is equal to 2. This theorem makes use of the `NeZero n` typeclass hypothesis. It's an extension of the theorem `Fin.succ_one_eq_two` in standard library, which only applies for finite sequence of length `n+2`.
More concisely: For any natural number $n$ with $n \neq 0$, the successor of the first element in a finite sequence of length $n$ is equal to 2.
|
Fin.strictMono_iff_lt_succ
theorem Fin.strictMono_iff_lt_succ :
∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
StrictMono f ↔ ∀ (i : Fin n), f i.castSucc < f i.succ
The theorem `Fin.strictMono_iff_lt_succ` states that, for any natural number `n` and any type `α` that has a `Preorder` relation, a function `f` from `Fin (n + 1)` to `α` is strictly monotone if and only if the value of `f` at `i` is less than the value of `f` at `i + 1` for every `i` in `Fin n`. Here, `Fin (n + 1)` represents the set of natural numbers less than `n + 1`, `Fin.castSucc i` represents embedding `i` from `Fin n` into `Fin (n + 1)`, and `Fin.succ i` represents the successor of `i` in `Fin (n + 1)`.
More concisely: A function from `Fin (n+1)` to a type with a preorder relation is strictly monotone if and only if `f (Fin.castSucc i) < f (Fin.succ i)` for all `i` in `Fin n`.
|
Fin.castSucc_le_castSucc_iff
theorem Fin.castSucc_le_castSucc_iff : ∀ {n : ℕ} {a b : Fin n}, a.castSucc ≤ b.castSucc ↔ a ≤ b
The theorem `Fin.castSucc_le_castSucc_iff` states that for all natural numbers `n` and for any two elements `a` and `b` of the finite set `Fin n`, the embedding of `a` in `Fin (n+1)` is less than or equal to the embedding of `b` in `Fin (n+1)` if and only if `a` is less than or equal to `b`. In other words, it says that the order of elements in `Fin n` is preserved when they are embedded into `Fin (n+1)` using the `Fin.castSucc` function.
More concisely: For all natural numbers n and Finite set elements a, b in Fin n, a ≤ b if and only if Fin.castSucc a ≤ Fin.castSucc b in Fin (n+1).
|
Mathlib.Data.Fin.Basic._auxLemma.15
theorem Mathlib.Data.Fin.Basic._auxLemma.15 : ∀ {n : ℕ} [inst : NeZero n], (1 = 0) = (n = 1)
This theorem, `Mathlib.Data.Fin.Basic._auxLemma.15`, states that for every natural number `n` which is not zero (`NeZero n`), the equality `1 = 0` is equivalent to `n = 1`. In other words, asserting that one is equal to zero (which is obviously false in the standard natural number system) is the same as asserting that the non-zero natural number `n` is equal to one.
More concisely: For any non-zero natural number `n`, the equality `1 = 0` holds if and only if `n = 1`.
|
Fin.val_succEmb
theorem Fin.val_succEmb : ∀ {n : ℕ}, ⇑(Fin.succEmb n) = Fin.succ
This theorem, `Fin.val_succEmb`, states that for every natural number `n`, the function `Fin.succEmb n` when applied to a value behaves the same way as `Fin.succ`. In other words, the operation of applying the order embedding `Fin.succEmb n` on a value is equivalent to applying the function `Fin.succ` on that same value, where `Fin.succ` is a function that takes an element from `Fin n` to `Fin (n+1)` by incrementing its underlying natural number. This implies a consistent behavior between the strictly monotonic function and its corresponding order embedding in terms of advancing to the next element in the finite sequence `Fin n`.
More concisely: For every natural number `n`, the order embedding `Fin.succEmb n` and the successor function `Fin.succ` agree on their application to elements of `Fin n`, i.e., `Fin.succEmb (Fin.mk n x) = Fin.mk (n+1) (Fin.succ x)` for all `x : Fin n`.
|
Fin.liftFun_iff_succ
theorem Fin.liftFun_iff_succ :
∀ {n : ℕ} {α : Type u_1} (r : α → α → Prop) [inst : IsTrans α r] {f : Fin (n + 1) → α},
((fun x x_1 => x < x_1) ⇒ r) f f ↔ ∀ (i : Fin n), r (f i.castSucc) (f i.succ)
The theorem `Fin.liftFun_iff_succ` states that for any natural number `n`, any type `α`, and any relation `r` on `α` that is transitive, if we have a function `f` from `Fin (n + 1)` to `α`, then the property that `f` maintains the order, i.e., `f(x) < f(y)` implies `r(f(x), f(y))`, is equivalent to the property that for all `i` in `Fin n`, `r(f (Fin.castSucc i)) (f (Fin.succ i))` holds. Here, `Fin n` represents the finite set {0, 1, ..., n-1}, `Fin.castSucc i` is embedding of `i` from `Fin n` into `Fin (n+1)`, and `Fin.succ i` provides the successor of `i` in the finite set.
More concisely: For a transitive relation `r` on type `α` and natural number `n`, a function `f` from `Fin (n+1)` to `α` maintains the order `r` if and only if `r(f (Fin.castSucc i)) (f (Fin.succ i))` holds for all `i` in `Fin n`.
|
Fin.val_zero'
theorem Fin.val_zero' : ∀ (n : ℕ) [inst : NeZero n], ↑0 = 0
This theorem, `Fin.val_zero'`, states that for all natural numbers `n` with a non-zero typeclass instance, the value of zero casted into the `Fin n` type is equal to zero. This is a generalization of the `Fin.val_zero` theorem in the `Std` library, which only applies when `n` is equal to `n+1`. Here, we instead require a `NeZero n` typeclass hypothesis, which essentially insists that `n` is not equal to zero.
More concisely: For all natural numbers `n` with `NeZero n`, the zero value in the type `Fin n` equals the natural number zero.
|
Fin.castSucc_lt_or_lt_succ
theorem Fin.castSucc_lt_or_lt_succ : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.castSucc < p ∨ p < i.succ
The theorem `Fin.castSucc_lt_or_lt_succ` states that for any natural number `n`, and for any elements `p` from `Fin (n + 1)` and `i` from `Fin n`, either `i` when embedded in `Fin (n + 1)` using `Fin.castSucc` is less than `p`, or `p` is less than the successor of `i` in `Fin (Nat.succ n)`. In other words, it expresses a total order between the cast successor of `i` and the natural successor of `i`, relative to a given element `p`.
More concisely: For any natural numbers `n`, `i` in `Fin n`, and `p` in `Fin (n + 1)`, either `Fin.castSucc i < p` or `p < Fin.castSucc (i + 1)` holds in the total order of `Fin (Nat.succ n)`.
|
Fin.orderEmbedding_eq
theorem Fin.orderEmbedding_eq :
∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f g : Fin n ↪o α}, Set.range ⇑f = Set.range ⇑g → f = g
This theorem states that for any natural number 'n' and any type 'α' (where 'α' is a preorder), if 'f' and 'g' are two order embeddings from the finite set `Fin n` to 'α', then if the ranges of 'f' and 'g' (i.e., the set of all elements in 'α' that 'f' and 'g' can map to) are equal, then 'f' and 'g' must be equal. In other words, two order embeddings of a finite set into a preordered set are identical if they have the same range.
More concisely: If two order embeddings of a finite set into a preordered type have equal ranges, then they are equal.
|
Fin.val_cast_of_lt
theorem Fin.val_cast_of_lt : ∀ {n : ℕ} [inst : NeZero n] {a : ℕ}, a < n → ↑↑a = a
This theorem, `Fin.val_cast_of_lt`, states that for any natural number `n` which is not zero, and any natural number `a` such that `a` is less than `n`, when `a` is converted to the finite type `Fin (n + 1)`, the resulting value is still the original number `a`. In other words, the operation of casting a number to a finite type doesn't change the value of the number, as long as the original number is in the valid range of the finite type.
More concisely: For all natural numbers `n` and `a` with `a < n`, the conversion of `a` to the finite type `Fin (n + 1)` results in the same value.
|
Fin.strictAnti_iff_succ_lt
theorem Fin.strictAnti_iff_succ_lt :
∀ {n : ℕ} {α : Type u_1} [inst : Preorder α] {f : Fin (n + 1) → α},
StrictAnti f ↔ ∀ (i : Fin n), f i.succ < f i.castSucc
The theorem `Fin.strictAnti_iff_succ_lt` states that for any natural number `n`, and any type `α` that has a preorder relationship, a function `f` from the finite set of size `n + 1` to `α` is strictly antitone (for every pair of elements `a` and `b`, if `a` is less than `b` then `f(b)` is less than `f(a)`) if and only if for every element `i` in the finite set of size `n`, the value of the function at `i.succ` (the successor of `i`) is less than the value of the function at `i.castSucc` (the casted successor of `i`).
More concisely: For a natural number `n` and a preordered type `α`, a function `f` from the finite set of size `n+1` to `α` is strictly antitone if and only if for all `i` in the finite set of size `n`, `f(i.succ)` < `f(i.castSucc)`.
|
Fin.heq_fun_iff
theorem Fin.heq_fun_iff :
∀ {α : Sort u_1} {k l : ℕ} (h : k = l) {f : Fin k → α} {g : Fin l → α}, HEq f g ↔ ∀ (i : Fin k), f i = g ⟨↑i, ⋯⟩
This theorem states that for any type `α` and natural numbers `k` and `l` such that `k = l`, two functions `f` and `g` defined on the finite sets `Fin k` and `Fin l` and mapping to `α`, are heterogeneously equal (equivalent in the `HEq` sense) if and only if they are equal on each element of `Fin k`. Here, `Fin k` and `Fin l` are types representing finite sets with `k` and `l` elements, respectively, and `HEq` is a type in Lean for heterogeneous equality, which allows comparing terms of different types.
More concisely: For any type `α` and natural numbers `k = l`, functions `f : Fin k -> α` and `g : Fin l -> α` are heterogeneously equal if and only if `f(i) = g(i)` for all `i : Fin k`.
|
Fin.rev_involutive
theorem Fin.rev_involutive : ∀ {n : ℕ}, Function.Involutive Fin.rev
The theorem `Fin.rev_involutive` states that for any natural number `n`, the `Fin.rev` function is involutive. In other words, applying the `Fin.rev` function twice to any input will return the original input. Specifically, `Fin.rev` is a function that maps `0` to `n-1`, `1` to `n-2`, and so forth up to `n-1` to `0` for any natural number `n`. So, the theorem essentially says that reversing the order twice brings you back to the original order.
More concisely: The `Fin.rev` function on natural numbers is idempotent, i.e., `Fin.rev (Fin.rev n) = n` for all natural numbers `n`.
|
Fin.val_fin_le
theorem Fin.val_fin_le : ∀ {n : ℕ} {a b : Fin n}, ↑a ≤ ↑b ↔ a ≤ b
This theorem states that for any natural number `n` and any two finite numbers `a` and `b` in the set `Fin n`, `a` is less than or equal to `b` as natural numbers if and only if `a` is less than or equal to `b` in the finite set `Fin n`. In other words, the comparison of `a` and `b` in terms of "less than or equal to" remains consistent whether they are treated as natural numbers or as elements of a finite number set.
More concisely: For any natural number `n` and `a, b` in `Fin n`, `a ≤ b` as natural numbers if and only if `a ≤ b` in `Fin n`.
|