Fin.succ_succAbove_one
theorem Fin.succ_succAbove_one :
∀ {n : ℕ} [inst : NeZero n] (i : Fin (n + 1)), i.succ.succAbove 1 = (i.succAbove 0).succ
This theorem, `Fin.succ_succAbove_one`, states that for any non-zero natural number `n` and any finite number `i` in the range from `0` to `n+1`, the successor of the successor of `i` above `1` is equal to the successor of `i` above `0`. In other words, with the `succ` function moved to the outside, this theorem provides a base for further simplification possibilities using the `succAbove_zero` or `succ_succAbove_zero` theorems in Lean 4.
More concisely: For any natural number `n` and finite index `i` in the range `0` to `n+1`, `(succ (succ i)) = succ (i + 1)`.
|
Fin.strictMono_succAbove
theorem Fin.strictMono_succAbove : ∀ {n : ℕ} (p : Fin (n + 1)), StrictMono p.succAbove
The theorem `Fin.strictMono_succAbove` states that for any natural number `n` and for any value `p` of type `Fin (n + 1)`, the function `Fin.succAbove p` is strictly monotone. In other words, if `a` and `b` are two elements of `Fin n` such that `a < b`, then `Fin.succAbove p a < Fin.succAbove p b`. This function `Fin.succAbove p` embeds `Fin n` into `Fin (n + 1)` leaving a gap at `p`, and it respects the ordering in `Fin n`, that is, smaller elements map to smaller elements and larger elements map to larger elements, with strict inequality preserved.
More concisely: For any natural number `n` and `p` in `Fin (n + 1)`, the function `Fin.succAbove p : Fin n -> Fin (n + 1)` is a strict monotonic embedding, meaning `a < b` in `Fin n` implies `Fin.succAbove p a < Fin.succAbove p b`.
|
Fin.succAbove_ne
theorem Fin.succAbove_ne : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p.succAbove i ≠ p
The theorem `Fin.succAbove_ne` states that for any natural number `n`, and any elements `p` of the finite set of size `n+1` and `i` of the finite set of size `n`, embedding `i` into the larger set with a hole around `p` using the `Fin.succAbove` function never results in `p` itself. In other words, the process of embedding maintains the distinctiveness of `p` and the embedded `i`.
More concisely: For all natural numbers n, and all i in Fin (n), and p in Fin (n+1), p is not in the image of i under the Fin.succAbove function.
|
Fin.succAbove_right_injective
theorem Fin.succAbove_right_injective : ∀ {n : ℕ} {x : Fin (n + 1)}, Function.Injective x.succAbove
The theorem `Fin.succAbove_right_injective` states that for any given natural number `n` and any fixed pivot `x : Fin (n + 1)`, the function `x.succAbove` is injective. In other words, if `x.succAbove a = x.succAbove b`, then it must be the case that `a = b`. This implies that the function `x.succAbove` does not map distinct elements of `Fin(n + 1)` to the same value, ensuring uniqueness in the mapping.
More concisely: For any natural number `n` and `x : Fin (n + 1)`, the function `x.succAbove : Fin (n) → Fin (n + 1)` is an injection.
|
Fin.succAbove_lt_ge
theorem Fin.succAbove_lt_ge : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.castSucc < p ∨ p ≤ i.castSucc
This theorem states that for any natural number `n`, and for any pair of finite numbers `p` and `i` such that `p` is a finite number over `n+1` and `i` is a finite number over `n`, either `i` cast to `n+1` is less than `p` or `p` is less than or equal to `i` cast to `n+1`. In other words, it establishes the comparison between a specific finite number and another finite number cast to the set of the next higher natural number.
More concisely: For any natural number `n`, and finite numbers `p` and `i` over `n`, either `i <= p` or `p < i` hold in the natural numbers `n+1`.
|
Fin.predAbove_of_castSucc_lt
theorem Fin.predAbove_of_castSucc_lt :
∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.castSucc < i) (hi : optParam (i ≠ 0) ⋯), p.predAbove i = i.pred hi
This theorem, `Fin.predAbove_of_castSucc_lt`, states that for all natural numbers `n`, given a finite number `p` of order `n`, another finite number `i` of order `n+1`, and a proof `h` that `Fin.castSucc p` is less than `i`, and an optional parameter `hi` which defaults to the proof that `i ≠ 0`, then applying the function `Fin.predAbove` to `p` and `i` is equal to applying the function `Fin.pred` to `i` with the proof `hi`. Essentially, it's describing a specific condition under which the subtraction of one from `i` in the context of `Fin.predAbove` and `Fin.pred` will yield the same result.
More concisely: For all natural numbers `n`, if `p` is a finite number of order `n`, `i` is a finite number of order `n+1`, and `Fin.castSucc p` is less than `i` with proof `h`, then `Fin.predAbove p i h` equals `Fin.pred i (option.some h)` (or `Fin.pred i h` if `i ≠ 0`).
|
Fin.succAbove_pred_of_lt
theorem Fin.succAbove_pred_of_lt :
∀ {n : ℕ} (p i : Fin (n + 1)) (h : p < i) (hi : optParam (i ≠ 0) ⋯), p.succAbove (i.pred hi) = i
This theorem states that for any natural number `n`, and any two elements `p` and `i` of the finite set `Fin (n + 1)`, if `p` is less than `i` and `i` is not zero (with an optional parameter to specify this), then the result of applying the function `Fin.succAbove` to `p` and the predecessor of `i` (`Fin.pred i`) is `i` itself.
In other words, embedding the predecessor of `i` into `Fin (n + 1)` with a hole around `p` through the `Fin.succAbove` function returns `i` if `p` is less than `i` and `i` is not zero. This is a property of the `Fin.succAbove` function and how it interacts with the `Fin.pred` function in the scope of finite sets.
More concisely: For any natural number `n` and `i, p` in `Fin (n + 1)` with `p < i` and `i ≠ 0`, `Fin.succAbove p (Fin.pred i) = i`.
|
Fin.succAbove_castSucc_of_le
theorem Fin.succAbove_castSucc_of_le : ∀ {n : ℕ} (p i : Fin n), p ≤ i → p.castSucc.succAbove i = i.succ
This theorem states that for all natural numbers `n` and for any two elements `p` and `i` of the finite set of size `n` (denoted as `Fin n`), if `p` is less than or equal to `i`, then embedding `Fin n` into `Fin (n+1)` with a hole around `p` using the `succAbove` function on `p` after it is embedded into `Fin (n+1)` using the `castSucc` function, and `i`, is equivalent to directly incrementing `i` by one using the `succ` function. In simpler terms, if we have a position `p` and another position `i` in a finite set, and `p` is not greater than `i`, then moving `p` up to the next set and then putting `i` in its place is the same as directly moving `i` up to the next set.
More concisely: For all natural numbers `n` and `p`, `i` in `Fin n`, if `p <= i`, then `succAbove p (castSucc i) = succ i` in `Fin (n+1)`.
|
Fin.succAbove_left_injective
theorem Fin.succAbove_left_injective : ∀ {n : ℕ}, Function.Injective Fin.succAbove
The theorem `Fin.succAbove_left_injective` states that for every natural number `n`, the function `Fin.succAbove` is injective. In other words, given any two elements from the finite set `Fin n`, if their images under the function `Fin.succAbove` are equal, then the two original elements must have been equal. Specifically, `Fin.succAbove` is a function that embeds the set `Fin n` into `Fin (n + 1)`, creating a 'hole' at a certain position, and this theorem asserts that different elements of `Fin n` will be mapped to different positions in `Fin (n + 1)`, maintaining distinctiveness.
More concisely: The function `Fin.succAbove` from `Fin n` to `Fin (n + 1)` is injective.
|
Fin.succAbove_of_castSucc_lt
theorem Fin.succAbove_of_castSucc_lt :
∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.castSucc < p → p.succAbove i = i.castSucc
This theorem states that for any natural number `n` and any two elements `p` from `Fin (n + 1)` and `i` from `Fin n`, if embedding `i` into `Fin (n + 1)` using the function `castSucc` results in a value that is less than `p`, then embedding `i` into `Fin (n + 1)` with a hole around `p` using the function `succAbove` is equivalent to the original embedding using `castSucc`. In other words, when the embedded value of `i` by `castSucc` is less than `p`, `succAbove` uses `castSucc` for embedding.
More concisely: If `i < p` in `Fin (n + 1)`, then `succAbove i p = castSucc i`.
|
Fin.succ_succAbove_succ
theorem Fin.succ_succAbove_succ :
∀ {n : ℕ} (i : Fin (n + 1)) (j : Fin n), i.succ.succAbove j.succ = (i.succAbove j).succ
The theorem `Fin.succ_succAbove_succ` states that for all natural numbers `n`, and for any two elements `i` of the finite set `Fin (n + 1)` and `j` of `Fin n`, the `succ` function, which increments an element of a finite set, commutes with the `succAbove` function. In other words, first applying `succ` to `i` and `j` and then applying `succAbove`, yields the same result as first applying `succAbove` to `i` and `j` and then applying `succ`. This can be represented in mathematical notation as `succAbove (succ i) (succ j) = succ (succAbove i j)`.
More concisely: For all natural numbers `n` and `i` in `Fin (n + 1)` and `j` in `Fin n`, `succAbove (succ i) (succ j) = succ (succAbove i j)`.
|
Fin.succAbove_zero
theorem Fin.succAbove_zero : ∀ {n : ℕ}, Fin.succAbove 0 = Fin.succ
The theorem `Fin.succAbove_zero` states that for every natural number `n`, the function `Fin.succAbove 0`, which embeds `Fin n` into `Fin (n + 1)` with a gap at zero, is equivalent to the function `Fin.succ`. In other words, when the hole is at zero, the `Fin.succAbove` function behaves the same as the `Fin.succ` function, which essentially adds 1 to every element of `Fin n`, therefore embedding `Fin n` into `Fin (n + 1)`.
More concisely: For every natural number `n`, the function `Fin.succAbove 0` on `Fin n` is equal to the successor function `Fin.succ`.
|
Fin.succAbove_lt_gt
theorem Fin.succAbove_lt_gt : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.castSucc < p ∨ p < i.succ
This theorem, named `Fin.succAbove_lt_gt`, states that for any natural number `n`, and for any `p` and `i` which are elements of the finite set of size `n+1` and `n` respectively, either the successor of `i` (with the successor operation defined in the context of finite sets, not just natural numbers) is less than `p` or `p` is less than the successor of `i`. In other words, in the ordered set of `n+1` elements, either `p` comes before the successor of `i` or it comes after.
More concisely: For any natural number $n$ and elements $i, p$ of a finite set of size $n+1$, either $p < i^{\prime}$ or $i^{\prime} < p$, where $i^{\prime}$ is the successor of $i$.
|
Fin.predAbove_succ_of_le
theorem Fin.predAbove_succ_of_le : ∀ {n : ℕ} (p i : Fin n), p ≤ i → p.predAbove i.succ = i
The theorem `Fin.predAbove_succ_of_le` states that for any natural number `n` and any two elements `p` and `i` from the finite set of size `n`, if `p` is less than or equal to `i`, then the result of applying the `predAbove` function to `p` and the successor of `i` is `i`. The `predAbove` function surjects `i` from `Fin (n+1)` into `Fin n` by subtracting one if `p` is less than `i`. The `succ` function adds one to `i`, turning an element of `Fin n` into an element of `Fin (n+1)`.
More concisely: For all natural numbers n and Fin n elements p and i, if p ≤ i then predAbove p (succ i) = i.
|
Fin.succAbove_of_le_castSucc
theorem Fin.succAbove_of_le_castSucc :
∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p ≤ i.castSucc → p.succAbove i = i.succ
The theorem `Fin.succAbove_of_le_castSucc` states that for any natural number `n`, and any elements `p` of type `Fin (n + 1)` and `i` of type `Fin n`, if `p` is less than or equal to the embedding of `i` into `Fin (n + 1)` (denoted by `Fin.castSucc i`), then the embedding of `i` into `Fin (n + 1)` with a hole around `p` (denoted by `Fin.succAbove p i`) is equal to the successor of `i` (denoted by `Fin.succ i`). In simpler terms, it says that when we try to embed `i` into a larger set with a hole at `p`, if `p` is not greater than `i`, the hole doesn't affect the position of `i` in the larger set.
More concisely: For any natural numbers `n`, `i`, and `p` with `i < p <= Fin.castSucc i` in `Fin (n + 1)`, `Fin.succAbove p i` equals `Fin.succ i`.
|
Fin.succAbove_left_inj
theorem Fin.succAbove_left_inj : ∀ {n : ℕ} {x y : Fin (n + 1)}, x.succAbove = y.succAbove ↔ x = y
The theorem `Fin.succAbove_left_inj` states that the function `succAbove` is injective at the pivot for any natural number `n` and any two elements `x` and `y` of the type `Fin (n + 1)`. In other words, if `x.succAbove` equals `y.succAbove`, then `x` must be equal to `y`, and vice versa.
More concisely: For all natural numbers `n` and elements `x` and `y` of `Fin (n + 1)`, if `x.succAbove = y.succAbove`, then `x = y`.
|
Fin.succAbove_predAbove
theorem Fin.succAbove_predAbove :
∀ {n : ℕ} {p : Fin n} {i : Fin (n + 1)}, i ≠ p.castSucc → p.castSucc.succAbove (p.predAbove i) = i
This theorem states that for any natural number `n`, and for any two finite ordinal numbers `p` and `i` (where `i` is in the interval `[0, n+1]` and `p` is in the interval `[0, n]`), if `i` is not equal to the successor of `p`, then the operation of first decreasing `i` by one if it is above `p`, and then increasing it back by one (leaving a gap around `p`), results in the original number `i`. Essentially, this operation is an identity function for all elements other than the successor of `p`.
More concisely: For any natural number `n`, and finite ordinal numbers `p` and `i` in the intervals `[0, n]` and `[0, n+1]` respectively, if `i` is not the successor of `p`, then decreasing `i` if it is greater than `p` and then increasing it back by one equals `i`.
|
Fin.succAbove_of_succ_le
theorem Fin.succAbove_of_succ_le : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), i.succ ≤ p → p.succAbove i = i.castSucc
The theorem `Fin.succAbove_of_succ_le` states that for any natural number `n` and any two finite ordinal numbers `p` and `i` of orders `n + 1` and `n` respectively, if the successor of `i` is less than or equal to `p`, then the operation of embedding `i` into `Fin (n + 1)` with a hole around `p` (i.e., `Fin.succAbove p i`) is equivalent to the operation of embedding `i` into `Fin (n + 1)` directly (i.e., `Fin.castSucc i`). In mathematical terms, if `succ(i) ≤ p`, then `succAbove(p, i) = castSucc(i)`.
More concisely: If `n` is a natural number, `p` is a finite ordinal of order `n + 1`, and `i` is a finite ordinal of order `n` with `succ(i) ≤ p`, then `Fin.succAbove p i = Fin.castSucc i`.
|
Fin.succAbove_last
theorem Fin.succAbove_last : ∀ {n : ℕ}, (Fin.last n).succAbove = Fin.castSucc
This theorem is stating that for any natural number `n`, the function `Fin.succAbove` with `Fin.last n` as its argument is equivalent to the function `Fin.castSucc`. In other words, if you embed the finite set `Fin n` into the finite set `Fin (n + 1)` and leave a hole at the greatest value of `Fin (n+1)`, which is `last n`, it is the same as directly embedding `Fin n` into `Fin (n+1)` using the `castSucc` function. This fundamentally says that the embedding by `castSucc` is the same as the embedding by `succAbove` with a hole at the last element.
More concisely: For any natural number `n`, the functions `Fin.succAbove` applied to `Fin.last n` and `Fin.castSucc` are equivalent.
|
Fin.range_succAbove
theorem Fin.range_succAbove : ∀ {n : ℕ} (p : Fin (n + 1)), Set.range p.succAbove = {p}ᶜ
For any natural number `n` and a `p` of type `Fin (n + 1)`, the theorem `Fin.range_succAbove` states that the range of the function `p.succAbove` comprises all elements except `p`. In other words, the set of all possible values that `p.succAbove` can take is the complement of the set containing only `p`.
More concisely: The theorem `Fin.range_succAbove` asserts that the function `p.succAbove` on `Fin (n + 1)` omits the element `p`.
|
Fin.predAbove_of_lt_succ
theorem Fin.predAbove_of_lt_succ :
∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i < p.succ) (hi : optParam (i ≠ Fin.last n) ⋯),
p.predAbove i = i.castPred hi
This theorem, `Fin.predAbove_of_lt_succ`, states for any natural number `n`, given `p` of type `Fin n` and `i` of type `Fin (n + 1)`. If `i` is less than `p + 1` (expressed as `Fin.succ p`), and if there exists a value (which is optional) confirming that `i` is not equal to the maximum possible value of `Fin (n + 1)` (expressed as `Fin.last n`), then applying the function `Fin.predAbove` with parameters `p` and `i` yields the same result as applying the `Fin.castPred` function on `i` with the confirmation that `i` is not the maximum value. In other words, under these conditions, these two functions behave identically.
More concisely: If `i < Fin.succ p` in `Fin (n + 1)` and `i ≠ Fin.last (n + 1)`, then `Fin.predAbove p i = Fin.castPred i`.
|
Fin.succAbove_castPred_of_lt
theorem Fin.succAbove_castPred_of_lt :
∀ {n : ℕ} (p i : Fin (n + 1)) (h : i < p) (hi : optParam (i ≠ Fin.last n) ⋯), p.succAbove (i.castPred hi) = i := by
sorry
The theorem `Fin.succAbove_castPred_of_lt` states that for any natural number `n` and any two elements `p` and `i` of the type `Fin (n + 1)`, if `i` is less than `p` and `i` is not the last element of `Fin (n + 1)` (with the latter condition being optional and defaults to a certain value if not given), then embedding `Fin n` into `Fin (n + 1)` with a hole around `p` after casting `i` from `Fin (n + 1)` to `Fin n` results in `i` itself. In simpler terms, if `i` is less than `p` and is not the biggest element, then inserting `i` in `Fin n` (after reducing its size by 1) into `Fin (n + 1)` at position `p` will give us `i` again.
More concisely: For any natural numbers `n` and `i`, `p` in `Fin (n + 1)` with `i < p` and `i ≠ last (Fin (n + 1))`, the embedding of `i` from `Fin (n + 1)` to `Fin n` and back to `Fin (n + 1)` at position `p` yields `i`.
|
Fin.predAbove_succAbove
theorem Fin.predAbove_succAbove : ∀ {n : ℕ} (p i : Fin n), p.predAbove (p.castSucc.succAbove i) = i
This theorem states that for any two elements `p` and `i` of the finite set `Fin n` (which contains `n` elements), if we first map `Fin n` to `Fin (n + 1)` by inserting an element at position `p` (`p.castSucc.succAbove i`), and then map `Fin (n + 1)` back to `Fin n` by removing the inserted element (`p.predAbove`), we get back the original element `i`. Essentially, these two operations are inverses of each other.
More concisely: For all `n`, `p`, and `i` in `Fin n`, the operations `p.castSucc.succAbove` and `p.predAbove` on `Fin n` form an inverse pair, that is, `p.predAbove (p.castSucc.succAbove i) = i` and `p.castSucc.succAbove (p.predAbove i) = i`.
|
Fin.succAbove_of_lt_succ
theorem Fin.succAbove_of_lt_succ : ∀ {n : ℕ} (p : Fin (n + 1)) (i : Fin n), p < i.succ → p.succAbove i = i.succ := by
sorry
The theorem `Fin.succAbove_of_lt_succ` states that for any natural number `n` and for two terms `p` and `i` of the types `Fin (n + 1)` and `Fin n` respectively, if `p` is less than the successor of `i`, then the result of the function `Fin.succAbove` applied to `p` and `i` is equal to the successor of `i`. In simpler terms, if `p` is less than the next number after `i`, then embedding `Fin n` into `Fin (n + 1)` with a hole around `p` is equivalent to just moving to the next number after `i`.
More concisely: For all natural numbers `n`, `i : Fin n`, and `p : Fin (n + 1)`, if `p < succ i`, then `Fin.succAbove p i = succ i`.
|
Fin.succ_predAbove_succ
theorem Fin.succ_predAbove_succ :
∀ {n : ℕ} (a : Fin n) (b : Fin (n + 1)), a.succ.predAbove b.succ = (a.predAbove b).succ
This theorem states that for any natural number `n` and any two finite sets `a` of size `n` and `b` of size `n + 1`, the `succ` function (which increments the value) commutes with the `predAbove` function when applied to `a` and `b`. Specifically, if we first increment `a` and then apply `predAbove` with respect to `b`, we get the same result as if we first applied `predAbove` to `a` with respect to `b` and then incremented the result.
More concisely: For any finite sets `a` and `b` of sizes `n` and `n+1` respectively, `predAbove (succ a) b` equals `predAbove a (succ b)`.
|
Fin.pred_succAbove_pred
theorem Fin.pred_succAbove_pred :
∀ {n : ℕ} {a : Fin (n + 2)} {b : Fin (n + 1)} (ha : a ≠ 0) (hb : b ≠ 0) (hk : optParam (a.succAbove b ≠ 0) ⋯),
(a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk
This theorem states that for any natural numbers `n`, `a` (of type `Fin (n + 2)`) and `b` (of type `Fin (n + 1)`) which are non-zero (denoted by `ha` and `hb`), the operation of `pred` (which decrement the value by 1) commutes with `succAbove` (which increment the value by 1). In other words, decrementing `a` and then incrementing the resultant value `b` is the same as first incrementing `a` and then decrementing the resultant value `b`. This statement holds under the optional condition that `a.succAbove b` is non-zero (denoted by `hk`) where `a.succAbove b` is not equal to zero as a default value for `hk`.
More concisely: For any natural numbers `n`, `a` of type `Fin (n + 2)` and `b` of type `Fin (n + 1)` which are non-zero, `pred (succAbove a b)` is equal to `succAbove (pred a) b` when `a.succAbove b` is non-zero.
|
Fin.succAbove_right_inj
theorem Fin.succAbove_right_inj : ∀ {n : ℕ} {i j : Fin n} (x : Fin (n + 1)), x.succAbove i = x.succAbove j ↔ i = j := by
sorry
This theorem states that for a given fixed pivot `x` of type `Fin (n + 1)`, the function `x.succAbove` is injective. In other words, if `x.succAbove i` equals `x.succAbove j` for some `i` and `j` of type `Fin n`, then `i` must be equal to `j`. Here, `Fin n` represents a finite set of natural numbers less than `n`.
More concisely: For any `x : Fin (n + 1)`, the function `x.succAbove : Fin n → Fin (n + 1)` is injective.
|
Fin.predAbove_castSucc_of_le
theorem Fin.predAbove_castSucc_of_le : ∀ {n : ℕ} (p i : Fin n), i ≤ p → p.predAbove i.castSucc = i
This theorem states that for any natural number `n` and for any two elements `p` and `i` of the finite set `Fin n` (which contains exactly `n` elements), if `i` is less than or equal to `p`, then if you first cast `i` to the set `Fin(n+1)` using `Fin.castSucc` and then apply the `Fin.predAbove` function on `p` and the result, you will end up with `i` again. This means that, under these conditions, `Fin.predAbove p (Fin.castSucc i)` is essentially a no-op.
More concisely: For any natural number `n` and elements `i` and `p` of `Fin n`, if `i ≤ p`, then `Fin.predAbove (Fin.castSucc i) p = i`.
|
Fin.predAbove_of_le_castSucc
theorem Fin.predAbove_of_le_castSucc :
∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : i ≤ p.castSucc) (hi : optParam (i ≠ Fin.last n) ⋯),
p.predAbove i = i.castPred hi
The theorem `Fin.predAbove_of_le_castSucc` states that for any natural number `n`, and any numbers `p` of type `Fin n` and `i` of type `Fin (n + 1)`, if `i` is less than or equal to the embedding of `p` in `Fin (n+1)` (`Fin.castSucc p`), then the operation `Fin.predAbove p i` is equivalent to subtracting one from `i` (`Fin.castPred i`) given that `i` is not the maximum value in `Fin (n+1)`. We can optionally specify `i` not equal to `Fin.last n` as an additional parameter (`hi`), which triggers the Lean 4 theorem prover to attempt to use this fact if it is not explicitly provided.
More concisely: For any natural numbers $n$, $p$ in $Fin(n)$, and $i$ in $Fin(n+1)$, if $i \leq \text{cast}_+(p)$ and $i \neq \text{last}(n+1)$, then $\text{predAbove}_p i = \text{castPred}\ i$.
|
Fin.predAbove_of_succ_le
theorem Fin.predAbove_of_succ_le :
∀ {n : ℕ} (p : Fin n) (i : Fin (n + 1)) (h : p.succ ≤ i) (hi : optParam (i ≠ 0) ⋯), p.predAbove i = i.pred hi := by
sorry
The theorem `Fin.predAbove_of_succ_le` states that for any natural number `n`, and any finite numbers `p` and `i` where `p` is of type `Fin n` and `i` is of type `Fin (n + 1)`, if the successor of `p` is less than or equal to `i`, and `i` is not zero (with an optional parameter default), then the result of calling the function `Fin.predAbove` with `p` and `i` as arguments is the same as the result of calling the function `Fin.pred` with `i` and the proof of `i` being non-zero as arguments. In other words, it asserts the equality of two specific operations on finite numbers when certain conditions on the numbers are satisfied.
More concisely: For any natural numbers `n`, `p` in `Fin n`, and `i` in `Fin (n + 1)`, if `p < i` and `i ≠ 0`, then `Fin.predAbove p i` equals `Fin.pred i (some (nat.dec_ne_zero i))`.
|
Fin.succAbove_pos
theorem Fin.succAbove_pos : ∀ {n : ℕ} [inst : NeZero n] (p : Fin (n + 1)) (i : Fin n), 0 < i → 0 < p.succAbove i := by
sorry
This theorem states that given a non-zero natural number `n`, a positive `Fin (n + 1)` element `p`, and a positive `Fin n` element `i`, embedding `i` above `p` using the `succAbove` function will result in a positive `Fin (n + 1)` element. In other words, if you have a positive element in a finite set of size `n` and you insert it into a larger set of size `n + 1` at a position indicated by a positive element from this larger set, the resulting element in the larger set is also positive.
More concisely: Given natural numbers `n`, `i`, and `p` with `0 < i <= n` and `0 < p <= n + 1`, `succAbove i p` is a positive element in `Fin (n + 1)`.
|