Fin.append_left_eq_cons
theorem Fin.append_left_eq_cons :
∀ {α : Type u_1} {n : ℕ} (x₀ : Fin 1 → α) (x : Fin n → α), Fin.append x₀ x = Fin.cons (x₀ 0) x ∘ Fin.cast ⋯ := by
sorry
This theorem states that for any type `α` and natural number `n`, if you have a function `x₀` that maps a one-element tuple (i.e., a `Fin 1`) into `α`, and another function `x` that maps an `n`-element tuple (i.e., a `Fin n`) into `α`, then appending the `n`-element tuple to the `1`-element tuple (using `Fin.append`) is equivalent to constructing a `n+1`-element tuple (i.e., a `Fin (n + 1)`) where the first element is the result of `x₀ 0` and the remaining elements come from `x`, with `x` appropriately mapped (using `Fin.cast`) to fit the new size of the tuple (`n + 1`). This process of constructing a `n+1`-element tuple is done using `Fin.cons`.
More concisely: For any type `α` and natural numbers `n` and `m` with `m > 0`, if `x₀ : α → Fin 1 → α` and `x : α → Fin n → α`, then `x₀ (Fin.cast (Fin.append (Fin.unit) (Fin.range m))) i = x 0 i ∧ x (Fin.cons i h) h' for all i : Fin m and h : Fin n and h' : Fin (m + n)`.
|
Fin.contractNth_apply_of_lt
theorem Fin.contractNth_apply_of_lt :
∀ {n : ℕ} {α : Type u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n),
↑k < ↑j → j.contractNth op g k = g k.castSucc
The theorem `Fin.contractNth_apply_of_lt` states that for any natural number `n`, any type `α`, any finite ordinal `j` of the form `Fin (n + 1)`, any binary operation `op` on `α`, any function `g` mapping `Fin (n + 1)` to `α`, and any finite ordinal `k` of the form `Fin n`, if the value of `k` is less than the value of `j`, then applying the function `Fin.contractNth` to `j`, `op`, `g`, and `k` yields the same result as applying `g` to the value obtained by embedding `k` into `Fin (n + 1)` using the function `Fin.castSucc`. In other words, it tells us how the function `Fin.contractNth` behaves when its `k` argument is less than its `j` argument.
More concisely: For any natural number `n`, any binary operation `op` on type `α`, any function `g : Fin (n + 1) → α`, and any finite ordinals `j : Fin (n + 1)` and `k : Fin n` with `k < j`, `Fin.contractNth j op g k` equals `g (Fin.castSucc k)`.
|
Fin.tail_update_succ
theorem Fin.tail_update_succ :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.succ),
Fin.tail (Function.update q i.succ y) = Function.update (Fin.tail q) i y
The theorem `Fin.tail_update_succ` states that for any natural number `n`, any function `q` that maps an `n+1` tuple to a particular type, any `n` tuple `i`, and any element `y` of the type at the next index of `i`, updating a non-zero element of the function and then taking the tail of the function (i.e., the last `n` entries) is the same as updating the tail of the function first and then taking the tail. In other words, the operations of updating a non-zero element and taking the tail of a function commute.
More concisely: For any natural number `n`, any function `q` from `(n+1) × Type → Type`, and `i : 팅 n`, `y : Type`, updating the `(n+1)`-th entry of `q` at index `i` and taking the tail equals taking the tail first and then updating the `n`-th entry. In symbols, `tail (update i y (update i x q)) = update i x (tail q)`.
|
Fin.find_eq_none_iff
theorem Fin.find_eq_none_iff :
∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p], Fin.find p = none ↔ ∀ (i : Fin n), ¬p i
The theorem `Fin.find_eq_none_iff` states that for any natural number `n` and any predicate `p` that applies to elements of the finite set `Fin n` (where `DecidablePred p` indicates that the predicate `p` is decidable), the function `Fin.find p` returns `none` if and only if the predicate `p` does not hold for any element `i` of the finite set `Fin n`. In other words, there is no element `i` in the set `Fin n` for which `p i` is true.
More concisely: For any finite set `Fin n` and decidable predicate `p` on `Fin n`, `Fin.find p` returns `none` if and only if `p` does not hold for any element of `Fin n`.
|
Fin.isSome_find_iff
theorem Fin.isSome_find_iff :
∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p], (Fin.find p).isSome = true ↔ ∃ i, p i
The theorem `Fin.isSome_find_iff` states that for every natural number `n` and a predicate `p` acting on a finite subset of `n`, where this predicate is decidable, the function `Fin.find p` will not return `none` if and only if there exists an index `i` such that the predicate `p i` holds true. In mathematical terms, this theorem provides a condition under which a decidable predicate is true for some index in a finite subset of the natural numbers.
More concisely: For a finite subset of natural numbers and a decidable predicate acting on it, `Fin.find p` returns some element if and only if there exists an index in the subset satisfying `p`.
|
Fin.update_cons_zero
theorem Fin.update_cons_zero :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α 0) (p : (i : Fin n) → α i.succ) (z : α 0),
Function.update (Fin.cons x p) 0 z = Fin.cons z p
This theorem states that for any natural number `n`, any function `α` from the set of `n+1` natural numbers to some type `u`, any `x` in the codomain of `α`, any function `p` from the set of `n` natural numbers to the successors in codomain of `α`, and any `z` in the codomain of `α`, adding an element `x` at the beginning of a tuple derived from function `p` and then updating that added element with `z` is equivalent to directly adding `z` at the beginning of the tuple derived from function `p`. In other words, the process of first consing `x` onto the tuple and then replacing it with `z` is the same as simply consing `z` onto the tuple in the first place.
More concisely: For any natural number `n`, any function `α : Nat → u`, any `x, z ∈ α (Nat.succ n)`, and any function `p : Nat → α (Nat.succ n)`, the tuples `(α (p 0) :: α (p 1) :: ... :: x :: z :: p (Nat.size !p) :: Nil)` and `(z :: α (p 0) :: α (p 1) :: ... :: α (p (Nat.pred !p)) :: x :: Nil)` are equal.
|
Fin.snoc.proof_2
theorem Fin.snoc.proof_2 : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (i : Fin (n + 1)), ¬↑i < n → α (Fin.last n) = α i
This theorem states that for any natural number `n` and any type `α` that depends on `Fin (n + 1)`, given any element `i` of `Fin (n + 1)`, if it is not the case that `i` is less than `n`, then the type `α` at `Fin.last n` (which represents the greatest value in `Fin (n + 1)`) is equal to the type `α` at `i`. In other words, if `i` is not less than `n`, it must be equal to `n`, and thus, it's type `α` is the same as that at `Fin.last n`.
More concisely: For any natural number `n` and type `α` that depends on `Fin (n + 1)`, if `i` is an element of `Fin (n + 1)` such that `i ≥ n`, then `α` at position `i` is equal to `α` at position `Fin.last n`.
|
Fin.insertNth_apply_succAbove
theorem Fin.insertNth_apply_succAbove :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)) (j : Fin n),
i.insertNth x p (i.succAbove j) = p j
The theorem `Fin.insertNth_apply_succAbove` states that for any natural number `n`, any type function `α` indexed by `Fin (n + 1)`, any index `i` in `Fin (n + 1)`, any element `x` of the type `α i`, any function `p` from `Fin n` to `α (Fin.succAbove i j)`, and any index `j` in `Fin n`, applying the function `Fin.insertNth` to the index `Fin.succAbove i j` is equivalent to applying the function `p` to the index `j`. In other words, inserting an element at a position determined by `Fin.succAbove i j` in a sequence using `Fin.insertNth` and then accessing the element at that position yields the same result as directly applying the function `p` to `j`.
More concisely: For any natural number `n`, any type function `α` indexed by `Fin (n + 1)`, any `i` in `Fin (n + 1)`, any `x` of type `α i`, any function `p` from `Fin n` to `α (Fin.succAbove i)`, and any `j` in `Fin n`, `Fin.insertNth (Fin.succAbove i j) x (p j) = p j`.
|
Mathlib.Data.Fin.Tuple.Basic._auxLemma.4
theorem Mathlib.Data.Fin.Tuple.Basic._auxLemma.4 :
∀ {α : Fin 0 → Sort u_1} {P : ((i : Fin 0) → α i) → Prop}, (∀ (x : (i : Fin 0) → α i), P x) = P finZeroElim := by
sorry
The theorem `Mathlib.Data.Fin.Tuple.Basic._auxLemma.4` states that for any dependent type `α` indexed over `Fin 0` (the finite set with zero elements) and any property `P` that applies to functions from indices in `Fin 0` to elements of `α`, if the property `P` holds for all such functions `x`, then specifically, it holds for the function `finZeroElim`. In other words, since there are no indices in `Fin 0`, any property that is said to hold for all functions from `Fin 0` to `α` must certainly hold for `finZeroElim`, which is the function defined to handle this empty-index situation.
More concisely: If a property `P` holds for all functions from `Fin 0` to a type `α`, then `P` holds for the function `finZeroElim` from `α` to itself.
|
Fin.tail_init_eq_init_tail
theorem Fin.tail_init_eq_init_tail :
∀ {n : ℕ} {β : Type u_1} (q : Fin (n + 2) → β), Fin.tail (Fin.init q) = Fin.init (Fin.tail q)
The theorem `Fin.tail_init_eq_init_tail` states that for any natural number `n` and any type `β`, if we have a function `q` mapping from a size `n+2` finite set to `β`, then taking the tail of the initial `n+1` elements of `q` (i.e., the last `n` elements) is equivalent to taking the initial `n+1` elements of the tail of `q` (i.e., the first `n` elements). In other words, the operations of 'tail' and 'init' commute with each other. This theorem is stated in a non-dependent setting to avoid type casting problems in Lean, making it easier to use.
More concisely: For any natural number `n` and type `β`, the tail of the first `n+1` elements of a function from a size `n+2` finite set to `β` is equal to the initial `n+1` elements of the function's tail.
|
Fin.append_right_eq_snoc
theorem Fin.append_right_eq_snoc :
∀ {α : Type u_1} {n : ℕ} (x : Fin n → α) (x₀ : Fin 1 → α), Fin.append x x₀ = Fin.snoc x (x₀ 0)
The theorem `Fin.append_right_eq_snoc` asserts that for any type `α` and any natural number `n`, if we append a one-tuple to the right of an `n`-tuple using the `Fin.append` function, it is equivalent to adding an element at the end of the `n`-tuple using the `Fin.snoc` function. The element added in the case of `Fin.snoc` is the only element of the one-tuple added in the case of `Fin.append`. This theorem establishes the consistency between two ways of extending the length of a tuple by one, either by appending a one-tuple or by 'snoc'ing an element.
More concisely: For any type `α` and natural number `n`, appending a one-element list to the right of an `n`-element list is equivalent to adding an element to the end of the `n`-element list.
|
Fin.insertNth_last'
theorem Fin.insertNth_last' :
∀ {n : ℕ} {β : Type v} (x : β) (p : Fin n → β), (Fin.last n).insertNth x p = Fin.snoc p x
This theorem, `Fin.insertNth_last'`, states that for any natural number `n` and any type `β`, if you have an element `x` of type `β` and a function `p` that maps each element of `Fin n` (finite set of elements from 0 to n-1) to `β`, then inserting `x` at the last position of the tuple (using `Fin.insertNth`) with `Fin.last n` (which gives the greatest value in `Fin (n+1)`) is equivalent to adding `x` at the end of the `n`-tuple to get an `n+1`-tuple (using `Fin.snoc`). In essence, it's saying that you can insert an element at the end of a tuple either by using `Fin.insertNth` with `Fin.last` or by using `Fin.snoc`, and these two methods are equivalent.
More concisely: For any natural number `n` and type `β`, the application of `Fin.snoc` to an `n`-tuple `ts` with an element `x` is equivalent to the application of `Fin.insertNth` to the same `n`-tuple `ts` and index `Fin.last n` with element `x`.
|
Fin.insertNth_zero'
theorem Fin.insertNth_zero' : ∀ {n : ℕ} {β : Type v} (x : β) (p : Fin n → β), Fin.insertNth 0 x p = Fin.cons x p := by
sorry
The theorem `Fin.insertNth_zero'` states that for all natural numbers `n` and for any type `β`, given an element `x` of type `β` and a function `p` mapping from the first `n` natural numbers to `β`, the operation of inserting `x` at the 0th position of a tuple generated by `p` using the `Fin.insertNth` function is equivalent to the operation of adding `x` at the beginning of the tuple using the `Fin.cons` function. In other words, `Fin.insertNth` with the insertion position as 0 behaves the same as `Fin.cons`.
More concisely: For all natural numbers `n` and type `β`, `Fin.insertNth 0 x (p x::p) = x :: p`, where `x` is an element of `β` and `p` is a function mapping the first `n` natural numbers to `β`.
|
Fin.cons_injective2
theorem Fin.cons_injective2 : ∀ {n : ℕ} {α : Fin (n + 1) → Type u}, Function.Injective2 Fin.cons
The theorem `Fin.cons_injective2` states that, for any natural number `n` and any function `α` from `Fin (n + 1)` to some type `u`, the `Fin.cons` function, considered as a binary function, is injective. In mathematical terms, if you add an element at the beginning of an `n`-tuple using `Fin.cons` to get an `n+1`-tuple, then no two different pairs of an element and an `n`-tuple will result in the same `n+1`-tuple. This injectivity property ensures that you can uniquely recover the original pair from the resulting `n+1`-tuple.
More concisely: For any natural number `n` and any function `α : Fin (n + 1) → u`, the function `Fin.cons : ∀ i : Fin n, α i → α (Fin.pred i) × α i → Fin (n + 1) × α i` is injective.
|
Fin.contractNth_apply_of_gt
theorem Fin.contractNth_apply_of_gt :
∀ {n : ℕ} {α : Type u_1} (j : Fin (n + 1)) (op : α → α → α) (g : Fin (n + 1) → α) (k : Fin n),
↑j < ↑k → j.contractNth op g k = g k.succ
The theorem `Fin.contractNth_apply_of_gt` states that for every natural number `n`, for every type `α`, for every finite ordinal `j` less than or equal to `n`, for every binary operation `op` on `α`, for every function `g` from finite ordinals less than or equal to `n` to `α`, and for every finite ordinal `k` less than `n`, if `j` is less than `k`, then applying the function `Fin.contractNth` with parameters `j`, `op`, `g` and `k` is equal to applying the function `g` to the successor of `k`. In other words, if the index `j` is less than `k`, then the `k`th element after contracting at `j` is just the successor of `k` under the function `g`.
More concisely: For all natural numbers $n$, types $\alpha$, finite ordinals $j, k$ with $j < k$, binary operations $op$ on $\alpha$, and functions $g$ from finite ordinals less than or equal to $n$ to $\alpha$, the application of `Fin.contractNth` with parameters $j$, $op$, $g$, and $k$ equals the application of $g$ to the successor of $k$.
|
Fin.snoc_last
theorem Fin.snoc_last :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc),
Fin.snoc p x (Fin.last n) = x
The theorem `Fin.snoc_last` states that for any natural number `n` and a family of types indexed by `Fin (n + 1)`, when you add an element `x` at the end of an `n`-tuple to get an `n+1`-tuple (via the function `Fin.snoc`), the element at the position of the greatest value of `Fin (n+1)` in the new tuple is indeed `x`. In other words, when you 'snoc' an element on to the end of a tuple, you can retrieve the same element by looking at the end of the new tuple.
More concisely: For any natural number `n` and an `n+1`-tuple `ts`, the element added using `Fin.snoc` to form the new tuple `ts'` is equal to the last element of `ts'`, i.e., `ts.last = Fin.snoc ts x`.
|
Fin.insertNth_rev
theorem Fin.insertNth_rev :
∀ {n : ℕ} {α : Type u_1} (i : Fin (n + 1)) (a : α) (f : Fin n → α) (j : Fin (n + 1)),
i.insertNth a f j.rev = i.rev.insertNth a (f ∘ Fin.rev) j
This theorem, `Fin.insertNth_rev`, states that for any natural number `n`, a type `α`, an element `i` of the type `Fin (n + 1)`, an element `a` of type `α`, a function `f` mapping from `Fin n` to `α`, and an element `j` of the type `Fin (n + 1)`, inserting an element `a` at the position `i` in a tuple (with the help of function `f`) and then reversing the tuple (using `Fin.rev j`) is equivalent to reversing the position `i` (with `Fin.rev i`), inserting the same element `a` and then applying the function `f` composed with the reversal function `Fin.rev` to the tuple at position `j`. This theorem highlights the commutative property of the operation of insertion and reversal in the context of tuples.
More concisely: For any natural number `n`, any `α`, `i ∈ Fin (n + 1)`, `a ∈ α`, `f : Fin n → α`, and `j ∈ Fin (n + 1)`, the tuples `(f (Fin.rev i) :: f <$> Fin.init (Fin.drop i (Fin.enumFromTo 0 (n + 1))) ++ [a] ++ Fin.drop i (Fin.enumFromTo 0 n) ++ [f (Fin.rev j)] ++ map f (Fin.init (Fin.drop (succ i) (Fin.enumFromTo 0 n))) ++ [f (Fin.last (Fin.drop (succ i) (Fin.enumFromTo 0 n)))] and `(Fin.rev j, a) ++ map f (Fin.init (Fin.drop (pred i) (Fin.enumFromTo 0 n))) ++ [f i] ++ reverse (Fin.drop i (Fin.enumFromTo 0 n)) ++ [f (Fin.last (Fin.drop (pred i) (Fin.enumFromTo 0 n)))]` are equal.
|
Fin.tail_cons
theorem Fin.tail_cons :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α 0) (p : (i : Fin n) → α i.succ), Fin.tail (Fin.cons x p) = p
The theorem `Fin.tail_cons` states that for any natural number `n` and any type function `α` from `Fin (n + 1)` to a type `u`, given an element `x` of type `α 0` and a function `p : (i : Fin n) → α (Fin.succ i)`, the tail of the tuple obtained by adding `x` at the beginning of the `n`-tuple created by `p` is equal to `p` itself. In other words, the function `Fin.tail` applied to the `n+1`-tuple created by `Fin.cons x p` is equal to the original function `p`.
More concisely: For any natural number `n` and function `p : Fin (n + 1) → α`, the tail of the list `[x] @ map Fin.succ p` is equal to `p`.
|
Fin.snoc_castSucc
theorem Fin.snoc_castSucc :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n),
Fin.snoc p x i.castSucc = p i
This theorem states that for any natural number `n` and any dependent type `α : Fin (n + 1) → Type u`, given an object `x` of type `α (Fin.last n)` (i.e., `x` is an element of the type indexed by the last element of `Fin (n+1)`), a function `p : (i : Fin n) → α (Fin.castSucc i)` (i.e., `p` maps each element of `Fin n` after being embedded into `Fin (n+1)` to an object of the corresponding type in `α`), and an element `i` of `Fin n`, applying `Fin.snoc` to `p`, `x`, and the embedded element `Fin.castSucc i` results in the same value as applying `p` to `i`. In essence, this theorem proves a property of the `Fin.snoc` operation which adds an element at the end of an `n`-tuple, showing that it behaves as expected when applied to an element that isn't the additional end element.
More concisely: For any natural number `n` and dependent type `α : Fin (n + 1) → Type u`, given an element `x : α (Fin.last n)`, a function `p : Fin n → α (Fin.castSucc i)`, and `i : Fin n`, `Fin.snoc p x (Fin.castSucc i) = p i`.
|
Fin.init_snoc
theorem Fin.init_snoc :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc),
Fin.init (Fin.snoc p x) = p
The theorem `Fin.init_snoc` states that for any natural number `n` and any function `α` that maps each element of the type `Fin (n + 1)` to a type `u`, for any element `x` of type `α` at the greatest value of `Fin (n+1)`, and any function `p` that maps each element of `Fin n` to `α (Fin.castSucc i)`, the initial `n` entries (obtained by the function `Fin.init`) of the `n+1`-tuple formed by appending `x` at the end of the `n`-tuple (obtained by the function `Fin.snoc`) are equal to the `n` entries of the original `n`-tuple. In other words, adding an element at the end of an `n`-tuple does not change the first `n` elements.
More concisely: For any natural number `n` and function `α : Fin (n + 1) → Type_, the initial `n` entries of `α` restricted to `Fin n` are equal to the first `n` entries of the `n+1`-tuple obtained by appending an element `x` of type `α (Fin.max)` to an `n`-tuple `p : ∀ i : Fin n, α (Fin.castSucc i)`.
|
Fin.sigma_eq_of_eq_comp_cast
theorem Fin.sigma_eq_of_eq_comp_cast :
∀ {α : Type u_1} {a b : (ii : ℕ) × (Fin ii → α)} (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h → a = b
This theorem, `Fin.sigma_eq_of_eq_comp_cast`, states that for any type `α`, and any two sigma pairs of tuples `a` and `b` which are of type natural number `ℕ` and a function from `Fin` of that natural number to `α`, if the first elements of `a` and `b` are equal (denoted by `a.fst = b.fst`), and the second element of `a` (`a.snd`) is equal to the composition of the second element of `b` (`b.snd`) and `Fin.cast` applied to the equality between the first elements, then `a` is equal to `b`. In simpler terms, it means that two tuples are equal if their first elements are equal and their second elements are related via a cast function that embeds one `Fin` type into another equal `Fin` type.
More concisely: For any type `α` and natural numbers `n` and `m`, if `Fin n ↦ α` `a` and `Fin m ↦ α` `b` are sigma pairs such that `n = m` and `a.1 = b.1` imply `a.2 = b.2 ∘ Fin.cast (a.1 = b.1)`, then `a = b`.
|
Fin.cons_succ
theorem Fin.cons_succ :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n),
Fin.cons x p i.succ = p i
The theorem `Fin.cons_succ` states that for any natural number `n`, and any dependent function `α` of type `Fin (n + 1) → Type u`, if we have an element `x` of type `α 0` and a function `p` that maps from `Fin n` to `α (Fin.succ i)`, then for any element `i` of `Fin n`, applying the `Fin.cons` function to `x`, `p`, and `Fin.succ i` will yield the same result as applying the function `p` to `i`. In other words, when we add an element at the beginning of an `n`-tuple to get an `n+1`-tuple using `Fin.cons` and then increment an index from `Fin n` to `Fin (n + 1)`, the result is the same as if we directly apply the function `p` to the original index in `Fin n`.
More concisely: For any natural number `n`, any dependent type `α : Fin (n + 1) → Type u`, element `x : α 0`, and function `p : Fin n → α (Fin.succ i)`, the application of `Fin.cons x p (Fin.succ i)` equals `p i` for all `i` in `Fin n`.
|
Mathlib.Data.Fin.Tuple.Basic._auxLemma.6
theorem Mathlib.Data.Fin.Tuple.Basic._auxLemma.6 :
∀ {ι : Type u} {α : ι → Type v} [inst : (i : ι) → LE (α i)] {x y : (i : ι) → α i}, (x ≤ y) = ∀ (i : ι), x i ≤ y i
This theorem, `Mathlib.Data.Fin.Tuple.Basic._auxLemma.6`, states that for all types `ι` and a type `α` that is dependent on `ι`, given an instance of a less than or equal to (`LE`) relation for every `ι`-indexed member of `α`, then for any two functions `x` and `y` mapping from `ι` to `α`, the statement "`x` is less than or equal to `y`" is equivalent to saying "for all `i` in `ι`, `x(i)` is less than or equal to `y(i)`". In other words, `x` is considered less than or equal to `y` if `x` is less than or equal to `y` for every element in the index set.
More concisely: For any type `ι` and a dependent type `α`, if there is a given relation `LE` on every `ι`-indexed member of `α`, then `x ≤ y` in `α^ι` if and only if `x(i) ≤ y(i)` for all `i` in `ι`.
|
Fin.cons_update
theorem Fin.cons_update :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α 0) (p : (i : Fin n) → α i.succ) (i : Fin n) (y : α i.succ),
Fin.cons x (Function.update p i y) = Function.update (Fin.cons x p) i.succ y
The theorem `Fin.cons_update` states that for any natural number `n`, type `α` that maps an `n+1`-tuple to a type, an element `x` of type `α 0`, a function `p` that maps an `n`-tuple to `α i.succ`, an `n`-tuple `i`, and an element `y` of `α i.succ`, the operation of adding an element at the beginning of a tuple (using `Fin.cons`) after updating the tuple (using `Function.update`) is equivalent to updating the tuple after adding an element at the beginning. In other words, the operations of updating a tuple and adding an element at the beginning commute.
More concisely: For any natural number `n`, type `α`, element `x` of type `α`, function `p`, `n`-tuple `i`, and element `y` of `α (i : nat)`, the operations `Fin.cons (x :: i) (Function.update i y p)` and `Function.update (i ::) y (λ i => p i) (x :: i)` are equal in type `α ((i : nat) -> α i)`.
|
Fin.tail_update_zero
theorem Fin.tail_update_zero :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (z : α 0),
Fin.tail (Function.update q 0 z) = Fin.tail q
This theorem states that updating the first element of a tuple does not change the tail of the tuple. More formally, given a function `q` from the type `Fin (n + 1)` to some type `α i` (interpreted as a tuple of length `n + 1`), and a new value `z` for the first element (of type `α 0`), the tail of the updated tuple (obtained from `Function.update q 0 z`) is the same as the tail of the original tuple (`Fin.tail q`). Here, `Fin.tail` is a function that returns the last `n` entries of an `n+1` tuple, and `Function.update` is a function that replaces the value of a function at a given point by a given value.
More concisely: Given a tuple `q : α :: x₁ ... x\_n` and `z : α`, replacing the first element gives a new tuple with the same tail: `Function.update q 0 z = ⟨_, x₁, ..., x\_n⟩`.
|
Fin.insertNth_eq_iff
theorem Fin.insertNth_eq_iff :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} {i : Fin (n + 1)} {x : α i} {p : (j : Fin n) → α (i.succAbove j)}
{q : (j : Fin (n + 1)) → α j}, i.insertNth x p = q ↔ q i = x ∧ p = fun j => q (i.succAbove j)
The theorem `Fin.insertNth_eq_iff` states that for any natural number `n`, a type `α` indexed by `Fin (n + 1)`, an index `i` of type `Fin (n + 1)`, an element `x` of type `α i`, a function `p` from `Fin n` to `α` (where for each `j`, `α (Fin.succAbove i j)`), and another function `q` from `Fin (n + 1)` to `α`, then `Fin.insertNth i x p` being equal to `q` is equivalent to `q i` being equal to `x` and `p` being equal to a function such that for each `j`, it equals `q (Fin.succAbove i j)`. In other words, the function `q` is equal to the function that inserts `x` at position `i` in the sequence `p` if and only if `q i` is `x` and `p` is the sequence obtained from `q` by removing the element at position `i`.
More concisely: The theorem `Fin.insertNth_eq_iff` asserts that a function `q : Fin (n + 1) → α` equals the function obtained by inserting an element `x : α` at position `i : Fin (n + 1)` in another function `p : Fin n → α` if and only if `q i = x` and for all `j : Fin n`, `q (Fin.succAbove i j) = p j`.
|
Fin.snoc_update
theorem Fin.snoc_update :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (i : Fin n)
(y : α i.castSucc), Fin.snoc (Function.update p i y) x = Function.update (Fin.snoc p x) i.castSucc y
The theorem `Fin.snoc_update` states that for any function `p` that maps indices `i` of type `Fin n` to values of type `α i.castSucc`, any value `x` of type `α (Fin.last n)`, any index `i` of type `Fin n`, and any value `y` of type `α i.castSucc`, the process of first updating the function `p` at the index `i` with the value `y` and then adding the value `x` at the end of this updated function (i.e., `Fin.snoc (Function.update p i y) x`) is the same as the process of first adding the value `x` at the end of the function `p` and then updating this resulting function at the index `i.castSucc` with the value `y` (i.e., `Function.update (Fin.snoc p x) i.castSucc y`). This shows that updating a tuple and adding an element at the end commute.
More concisely: For any function `p : Fin n → α`, any `x : α`, any `i : Fin n`, and any `y : α`, the functions `Fin.snoc (Function.update p i y) x` and `Function.update (Fin.snoc p x) (i.castSucc) y` are equal.
|
Fin.snoc_init_self
theorem Fin.snoc_init_self :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i), Fin.snoc (Fin.init q) (q (Fin.last n)) = q := by
sorry
The theorem `Fin.snoc_init_self` states that for any natural number `n` and any function `q` mapping indices of a `n+1`-tuple to a type `α`, concatenating the initial segment of the tuple (obtained using `Fin.init`) with the last element of the tuple (obtained using `q (Fin.last n)`) yields the original tuple `q`. In other words, this theorem proves that we can reconstruct the original tuple from its initial segment and its last element, validating the operations of `Fin.snoc` and `Fin.init`.
More concisely: For any natural number `n` and function `q` from `Fin (n+1)` to type `α`, `Fin.init (Fin.uncons (Fin.cons (Fin.last n) n)) = q`.
|
Fin.update_snoc_last
theorem Fin.update_snoc_last :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α (Fin.last n)) (p : (i : Fin n) → α i.castSucc) (z : α (Fin.last n)),
Function.update (Fin.snoc p x) (Fin.last n) z = Fin.snoc p z
The theorem `Fin.update_snoc_last` states that for any natural number `n`, Fin type `α`, and given elements `x` and `z` of type `α (Fin.last n)` and a function `p` that maps each element of `Fin n` to `α i.castSucc`, the operation of adding an element at the beginning of a tuple using `Fin.snoc` and then updating it using `Function.update` with `z` at the position `Fin.last n` is the same as directly adding `z` at the beginning using `Fin.snoc`. In other words, adding an element and then updating it is equivalent to directly adding the updated element.
More concisely: For any natural number `n`, Fin type `α` element `z`, and function `p : Fin n → α.castSucc`, the operation `Function.update (Fin.snoc (Fin.map p Fin.enumFromTo ∥ (z : α (Fin.last n))) (Fin.last n) z)` equals `Fin.snoc (p (Fin.last n) :: Fin.map p (Fin.enumFromTo 0 (pred n))) ⊎ z`.
|
Fin.init_update_last
theorem Fin.init_update_last :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (z : α (Fin.last n)),
Fin.init (Function.update q (Fin.last n) z) = Fin.init q
This theorem, "Fin.init_update_last", states that for any natural number `n`, any dependent function `q` of type `α` indexed by `Fin (n + 1)`, and any value `z` of the type `α` at the index `Fin.last n`, updating the value of `q` at the index `Fin.last n` to be `z` does not change the initial `n` entries of the tuple. In other words, the initial part of the tuple, `Fin.init`, remains the same before and after updating the last element of the tuple.
More concisely: For any natural number `n`, any dependent function `q` of type `α` indexed by `Fin (n + 1)`, and any value `z` of type `α`, updating `q` at index `Fin.last n` to `z` preserves the initial `n` entries of `q`.
|
Fin.cons_eq_append
theorem Fin.cons_eq_append :
∀ {n : ℕ} {α : Type u_1} (x : α) (xs : Fin n → α),
Fin.cons x xs = Fin.append (Fin.cons x Fin.elim0) xs ∘ Fin.cast ⋯
The theorem `Fin.cons_eq_append` states that for any natural number `n` and any type `α`, if we have an element `x` of type `α` and a function `xs` that maps from `Fin n` to `α`, then adding the element `x` at the beginning of the `n`-tuple using `Fin.cons` is equivalent to appending a one-tuple containing `x` to the left of the `n`-tuple using `Fin.append`, and then mapping the resulting `n+1`-tuple to the `n`-tuple using `Fin.cast`. This proves that `Fin.cons` and `Fin.append` followed by `Fin.cast` are essentially the same operation.
More concisely: For any natural number `n` and type `α`, `Fin.cons (x : α) (xs : Fin n → α) = Fin.append ([x] : Fin (S Int.pred n) → α) xs` where `[x]` is a one-tuple containing `x`.
|
Fin.sigma_eq_iff_eq_comp_cast
theorem Fin.sigma_eq_iff_eq_comp_cast :
∀ {α : Type u_1} {a b : (ii : ℕ) × (Fin ii → α)}, a = b ↔ ∃ (h : a.fst = b.fst), a.snd = b.snd ∘ Fin.cast h := by
sorry
The theorem `Fin.sigma_eq_iff_eq_comp_cast` states that for any type α and for any two pairs `a` and `b` of natural numbers and functions from finite sets of those natural numbers to α, `a` equals `b` if and only if there exists a proof `h` that the first elements of `a` and `b` (the natural numbers) are equal and the second element of `a` (the function) equals the composition of the second element of `b` and the `Fin.cast` function with `h`. In simpler terms, the pairs are equal if the numbers are equal and the functions, after adjusting for possibly different domains via `Fin.cast`, are also equal.
More concisely: For any types α and pairs of functions from finite sets of natural numbers to α, `a` and `b`, `a = b` if and only if there exists an equality of their first components and `a.2 = b.2 ∘ Fin.cast h`, where `h` is the proof of their first components' equality.
|
Fin.cons_self_tail
theorem Fin.cons_self_tail :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i), Fin.cons (q 0) (Fin.tail q) = q
This theorem states that for any natural number `n` and any function `q` from `Fin (n + 1)` to some type `α`, concatenating the first element of the tuple generated by `q` with the tail of the same tuple (the last `n` entries of the tuple) yields the original tuple. In other words, it formalizes the idea that combining the first element of a sequence with the rest of the sequence should reproduce the original sequence. This is a fundamental property in the manipulation of sequences or tuples.
More concisely: For any natural number `n` and function `q` from `Fin (n + 1)` to type `α`, `q 0 :: tail q` equals `q`.
|
Fin.insertNth_apply_same
theorem Fin.insertNth_apply_same :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (i : Fin (n + 1)) (x : α i) (p : (j : Fin n) → α (i.succAbove j)),
i.insertNth x p i = x
The theorem `Fin.insertNth_apply_same` asserts that for any natural number `n`, any type function `α` indexed by `Fin (n + 1)`, any element `i` of `Fin (n + 1)`, any element `x` of `α i`, and any function `p` mapping elements of `Fin n` to `α (Fin.succAbove i j)`, when we insert `x` into the tuple defined by `p` at position `i` using `Fin.insertNth`, the value at position `i` of the resulting tuple is `x`. In other words, the inserted element `x` is exactly at the position `i` in the modified tuple.
More concisely: For any natural number `n`, any type function `α` indexed by `Fin (n + 1)`, any `i` in `Fin (n + 1)`, any `x` in `α i`, and any function `p : Fin n -> α (Fin.succAbove i j)`, the application `Fin.insertNth p i x` results in a tuple where the `i`-th element is `x`.
|
Fin.init_update_castSucc
theorem Fin.init_update_castSucc :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (q : (i : Fin (n + 1)) → α i) (i : Fin n) (y : α i.castSucc),
Fin.init (Function.update q i.castSucc y) = Function.update (Fin.init q) i y
This theorem states that for any natural number `n`, any function `q` from indices of length `n+1` to a sort `α`, any index `i` of length `n`, and any value `y` of sort `α` at `i.castSucc`, updating the value of `q` at `i.castSucc` to `y` and then taking the first `n` entries (the beginning) is the same as first taking the first `n` entries of `q` and then updating the value at `i` to `y`. This can be interpreted as the processes of updating a function value and taking the beginning part of the function commuting with each other.
More concisely: For any natural number `n`, any function `q` from indices of length `n+1` to sort `α`, any index `i` of length `n`, and any value `y` of sort `α`, updating the value of `q` at `i.castSucc` to `y` and then taking the first `n` entries of `q` is equivalent to first taking the first `n` entries of `q` and then updating the value at `i` to `y`.
|
Fin.forall_iff_succAbove
theorem Fin.forall_iff_succAbove :
∀ {n : ℕ} {p : Fin (n + 1) → Prop} (i : Fin (n + 1)),
(∀ (j : Fin (n + 1)), p j) ↔ p i ∧ ∀ (j : Fin n), p (i.succAbove j)
This theorem states that for any natural number `n`, any predicate `p` on 'finite numbers' less than or equal to `n + 1`, and any 'finite number' `i` less than or equal to `n + 1`, the predicate `p` holds for all 'finite numbers' less than or equal to `n + 1` if and only if `p` holds for `i` and for all 'finite numbers' `j` less than `n`, `p` holds for the result of the function `Fin.succAbove i j`. Here, `Fin.succAbove i j` is a function that 'embeds' a 'finite number' `j` from a set of size `n` into a set of size `n + 1`, preserving the order but placing a 'hole' at the position `i`.
More concisely: For any natural number `n`, predicate `p` on finite numbers up to `n+1`, and finite number `i` <= `n+1`, `p` holds for all finite numbers up to `n+1` if and only if `p(i)` holds and for all `j` < `n`, `p` holds for `Fin.succAbove i j`.
|
Fin.find_min
theorem Fin.find_min :
∀ {n : ℕ} {p : Fin n → Prop} [inst : DecidablePred p] {i : Fin n}, i ∈ Fin.find p → ∀ {j : Fin n}, j < i → ¬p j
The theorem `Fin.find_min` states that for a given natural number `n` and a predicate `p` over the finite set `Fin n`, if `find p` function returns an element `i` from `Fin n`, then the predicate `p` does not hold true for any element `j` from `Fin n` that is less than `i`. In other words, `i` is the smallest index for which the predicate `p` is true. This decision of the predicate `p` being true or false is determined by the instance `inst` of `DecidablePred p`.
More concisely: If `find (p : Fin n → Prop) (Fin.range n)` exists and equals `i` in `Fin n`, then for all `j` in `Fin n` with `j < i`, it is false that `p j`.
|
Fin.append_left
theorem Fin.append_left :
∀ {m n : ℕ} {α : Type u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin m), Fin.append u v (Fin.castAdd n i) = u i := by
sorry
The theorem `Fin.append_left` states that for all natural numbers `m` and `n`, and for any type `α`, if you have two functions `u : Fin m → α` and `v : Fin n → α`, and an element `i` of `Fin m`, when you append `u` and `v` and apply it to the result of casting `i` with addition by `n` (i.e., `Fin.append u v (Fin.castAdd n i)`), the result is the same as directly applying `u` to `i` (i.e., `u i`). Essentially, it says that when you extend the domain of `u` and `v` to `Fin (m + n)`, the values of the extended function on the original domain of `u` are unchanged.
More concisely: For all natural numbers m and n, and for any type α, the appended functions u : Fin m → α and v : Fin n → α satisfy u (Fin.castAdd n i) = Fin.append u v i for all i in Fin m.
|
Fin.find_spec
theorem Fin.find_spec : ∀ {n : ℕ} (p : Fin n → Prop) [inst : DecidablePred p] {i : Fin n}, i ∈ Fin.find p → p i := by
sorry
This theorem states that, given a natural number `n` and a predicate `p` over the finite set of natural numbers less than `n`, if the function `Fin.find` applied on `p` returns `some i` (i.e., a specific finite number `i` less than `n`), then the predicate `p` holds for `i`. Here, the predicate `p` is assumed to be decidable (i.e., for any `i` in `Fin n`, we can definitely say whether `p i` is true or false). The theorem is saying that `Fin.find` works correctly: if it claims that `i` is a correct output, then `p i` is indeed true.
More concisely: If `Fin.find` returns `some i` for a decidable predicate `p` over `Fin n`, then `p i` holds.
|
Fin.insertNth_binop
theorem Fin.insertNth_binop :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (op : (j : Fin (n + 1)) → α j → α j → α j) (i : Fin (n + 1)) (x y : α i)
(p q : (j : Fin n) → α (i.succAbove j)),
(i.insertNth (op i x y) fun j => op (i.succAbove j) (p j) (q j)) = fun j =>
op j (i.insertNth x p j) (i.insertNth y q j)
The theorem `Fin.insertNth_binop` states that for any natural number `n` and a type `α` that depends on a value in `Fin (n + 1)`, given a binary operation `op` that acts on elements of type `α`, an index `i` in `Fin (n + 1)`, and two values `x` and `y` of type `α i`, if we have two functions `p` and `q` that, for every index in `Fin n`, associate it with an element of type `α` that is indexed by `Fin.succAbove i j` (which essentially embeds `Fin n` in `Fin (n + 1)` with a gap around `i`), then applying `op` to the results of inserting `x` and `y` at position `i` in the sequences defined by `p` and `q` gives the same outcome as first applying `op` to `x` and `y` and to each corresponding pair of elements from `p` and `q`, and then inserting these results at position `i` in the sequence. This is essentially saying that the process of inserting values at a specific position in a sequence commutes with the given binary operation.
More concisely: For any natural number `n`, binary operation `op` on type `α`, index `i` in `Fin (n + 1)`, and values `x` and `y` of type `α i`, if we have functions `p` and `q` that associate elements of `Fin n` with elements of type `α` indexed by `Fin.succAbove i j`, then `op` on the elements inserted at position `i` in sequences `p` and `q` equals `op` on `x` and `y` and the corresponding elements from `p` and `q`, followed by insertion at position `i` in the sequence of the results.
|
Fin.append_right
theorem Fin.append_right :
∀ {m n : ℕ} {α : Type u_1} (u : Fin m → α) (v : Fin n → α) (i : Fin n), Fin.append u v (Fin.natAdd m i) = v i := by
sorry
This theorem, `Fin.append_right`, states that for any natural numbers `m` and `n`, and any type `α`, given two functions `u` and `v` that map from `Fin m` and `Fin n` to `α` respectively, and an instance `i` of `Fin n`, if we first apply the `Fin.natAdd` function to `i` with `m` as the argument, and then append the function `u` and `v` (using `Fin.append`), the result will be equivalent to applying the function `v` to `i` directly. This can be interpreted as appending `u` and `v` and then adding `m` to `i` on the left doesn't change the fact that `i` still maps to the same element of `α` in `v`.
More concisely: For any natural numbers `m` and `n`, and any type `α`, if `i : Fin n`, then `(v ∘ Fin.natAdd _ m) (u i) = v i` for functions `u : Fin m → α` and `v : Fin n → α`.
|
Fin.cons_zero
theorem Fin.cons_zero :
∀ {n : ℕ} {α : Fin (n + 1) → Type u} (x : α 0) (p : (i : Fin n) → α i.succ), Fin.cons x p 0 = x
The theorem `Fin.cons_zero` states that for any natural number `n`, and any indexed type `α` that depends on `Fin (n + 1)`, given an element `x` of type `α 0` and a function `p` that maps any value of type `Fin n` to `α` indexed by the successor of that value, if `Fin.cons` is applied to `x`, `p`, and `0`, the result will be `x`. In simpler terms, this theorem says that when we add an element at the beginning of an `n`-tuple using `Fin.cons`, the resulting tuple's first element (at index `0`) is the element we added.
More concisely: For any natural number `n` and indexed type `α` over `Fin (n + 1)`, the application of `Fin.cons` to an element `x` of type `α 0` and a function `p` mapping `Fin n` to `α` yields a tuple with the first element equal to `x`.
|
Fin.cons_snoc_eq_snoc_cons
theorem Fin.cons_snoc_eq_snoc_cons :
∀ {n : ℕ} {β : Type u_1} (a : β) (q : Fin n → β) (b : β), Fin.cons a (Fin.snoc q b) = Fin.snoc (Fin.cons a q) b
This theorem, `Fin.cons_snoc_eq_snoc_cons`, states that for any natural number `n`, and any type `β`, if we have an element `a` of type `β`, a function `q` from `Fin n` to `β`, and another element `b` of type `β`, then adding `a` at the beginning and `b` at the end using `Fin.cons` and `Fin.snoc` respectively is equivalent to first adding `a` at the beginning and then `b` at the end using `Fin.snoc` and `Fin.cons` respectively. In simpler words, the operations of appending at the beginning (`cons`) and appending at the end (`snoc`) commute with each other.
More concisely: For all natural numbers `n` and type `β`, the function `Fin.cons : β -> Fin n -> Fin (Suc n) -> Fin n -> β` and `Fin.snoc : β -> Fin n -> Fin (Suc n) -> Fin n -> β` satisfy `Fin.cons (a : β) (x :: xs : Fin n) (y : β) = Fin.snoc (Fin.cons a x y) xs`.
|
Fin.snoc_eq_append
theorem Fin.snoc_eq_append :
∀ {n : ℕ} {α : Type u_1} (xs : Fin n → α) (x : α), Fin.snoc xs x = Fin.append xs (Fin.cons x Fin.elim0)
The theorem `Fin.snoc_eq_append` states that for any natural number `n` and any type `α`, the operation of adding an element at the end of an `n`-tuple using `Fin.snoc` is equivalent to appending a one-tuple containing that element to the original `n`-tuple using `Fin.append` and `Fin.cons`. In other words, using `Fin.snoc` to add an element `x` to a tuple `xs` yields the same result as using `Fin.append` to append the tuple `Fin.cons x Fin.elim0` to `xs`.
More concisely: For any natural number `n` and type `α`, the operation `Fin.snoc (xs : α ^ n) x` equals `Fin.append x (xs : α ^ n)`.
|