TypeVec.append1_drop_last
theorem TypeVec.append1_drop_last : ∀ {n : ℕ} (α : TypeVec.{u_1} (n + 1)), α.drop.append1 α.last = α
This theorem, `TypeVec.append1_drop_last`, states that for any natural number `n` and any `n+1`-length type vector `α`, if we drop the last element of `α` to obtain a new vector, and then append the last element of `α` back to this vector, we get back the original vector `α`. In essence, it captures the property that dropping and then appending the last element of a vector does not change the original vector. This is analogous to the concept in list theory where if you take a list, remove the last element, and then append it back, you get the original list.
More concisely: For any type vector `α` of length `n+1`, appending the last element of `α` to the subvector obtained by dropping the last element results in the original vector `α`.
|
TypeVec.eq_of_drop_last_eq
theorem TypeVec.eq_of_drop_last_eq :
∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {β : TypeVec.{u_2} (n + 1)} {f g : α.Arrow β},
TypeVec.dropFun f = TypeVec.dropFun g → TypeVec.lastFun f = TypeVec.lastFun g → f = g
This theorem, `TypeVec.eq_of_drop_last_eq`, states that for any natural number `n`, and any two `n+1`-tuples of types `α` and `β`, if two arrows `f` and `g` from `α` to `β` have the same "drop function" and the same "last function", then these two arrows `f` and `g` are equal. The "drop function" is obtained by removing the first type from the arrow, and the "last function" is obtained by isolating the last type of the arrow. Essentially, this theorem establishes that an arrow in the category of `n+1`-tuples of types is determined by its effect on the initial `n` types and the last type.
More concisely: Given natural number `n` and `n+1`-tuples of types `α` and `β`, if two functions `f : α → β` and `g : α → β` have equal drop functions (i.e., remove the first component) and equal last functions, then `f = g`.
|
TypeVec.appendFun_id_id
theorem TypeVec.appendFun_id_id : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : Type u_1}, (TypeVec.id ::: id) = TypeVec.id := by
sorry
The theorem `TypeVec.appendFun_id_id` states that for any natural number `n`, any `n`-tuple of types `α` (represented as a function from a finite set of size `n` to types), and any type `β`, appending the identity function to the end of the `TypeVec.id` function (which is the identity function on `n`-tuples of types) results in the `TypeVec.id` function itself. In other words, it shows that appending an identity function does not change the original function on `n`-tuples of types.
More concisely: For any natural number `n` and any `n`-tuple of types `α`, the function `TypeVec.appendFun (λ i, α i) TypeVec.id` equals `TypeVec.id` where `TypeVec.id` is the identity function on `n`-tuples of types.
|
TypeVec.id_comp
theorem TypeVec.id_comp :
∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f : α.Arrow β), TypeVec.comp TypeVec.id f = f
The theorem `TypeVec.id_comp` states that for any natural number `n`, and any two `n`-tuples of types `α` and `β`, the composition of the identity function `TypeVec.id` and any function `f` from `α` to `β` (`TypeVec.Arrow α β`) is equal to the function `f` itself. This is the mathematical equivalent of the identity law for function composition, which in formula terms can be expressed as: `Id ∘ f = f`, where `Id` is the identity function and `f` is any function from `α` to `β`.
More concisely: For any natural number `n` and functions `f : αᵢ → βёрiginal subscript i = 1,…,n`, `TypeVec.id_comp αβ n f` is the equality of functions `TypeVec.id αᵢ αᵢ ∘ f αᵢ βoriginal subscript i = 1,…,n` and `f αᵢ βoriginal subscript i = 1,…,n`.
|
TypeVec.Arrow.ext
theorem TypeVec.Arrow.ext :
∀ {n : ℕ} {α : TypeVec.{u_1} n} {β : TypeVec.{u_2} n} (f g : α.Arrow β), (∀ (i : Fin2 n), f i = g i) → f = g := by
sorry
This theorem, `TypeVec.Arrow.ext`, states that for any two arrows (functions) 'f' and 'g' in the category of `TypeVec`, from 'α' to 'β', if they are point-wise equal (i.e., for every index 'i' in the finite set `Fin2 n`, 'f' at index 'i' equals 'g' at index 'i'), then the arrows 'f' and 'g' themselves are equal. In other words, it's an extensionality theorem for arrows in the category of `TypeVec`, asserting that two arrows are equal if they behave the same way on all inputs.
More concisely: In the category of TypeVec, two functions with the same point-wise behavior at all indices are equal.
|
TypeVec.appendFun_comp
theorem TypeVec.appendFun_comp :
∀ {n : ℕ} {α₀ : TypeVec.{u_1} n} {α₁ : TypeVec.{u_2} n} {α₂ : TypeVec.{u_3} n} {β₀ : Type u_1} {β₁ : Type u_2}
{β₂ : Type u_3} (f₀ : α₀.Arrow α₁) (f₁ : α₁.Arrow α₂) (g₀ : β₀ → β₁) (g₁ : β₁ → β₂),
(TypeVec.comp f₁ f₀ ::: g₁ ∘ g₀) = TypeVec.comp (f₁ ::: g₁) (f₀ ::: g₀)
The theorem `TypeVec.appendFun_comp` states that for any natural number `n` and any six categories `α₀`, `α₁`, `α₂`, `β₀`, `β₁`, `β₂` in `TypeVec n` and `Type`, and any two `TypeVec.Arrow`s `f₀` and `f₁` from `α₀` to `α₁` and `α₁` to `α₂` respectively, and two functions `g₀` and `g₁` from `β₀` to `β₁` and `β₁` to `β₂` respectively, the composition of `f₁` and `f₀` appended with the composition of `g₁` and `g₀` is equal to the composition of `f₁` appended with `g₁` and `f₀` appended with `g₀`.
In other words, the theorem is expressing a property of the composition operation in the category of `TypeVec n` and `Type`: the composition operation is associative and respects the concatenation (appending) of arrows. This is a basic property one would expect from a category, and is similar to function composition in set theory.
More concisely: For any natural number `n` and categories `α₀, α₁, α₂, β₀, β₁, β₂` in `TypeVec n` and `Type`, and functions `f₀ : α₀ → α₁`, `f₁ : α₁ → α₂`, `g₀ : β₀ → β₁`, and `g₁ : β₁ → β₂`, the diagram `(f₁ ∘ f₀) ∘ (g₁ ∘ g₀) ↔ (f₁ ∘ g₁) ∘ (f₀ ∘ g₀)` holds in the category of `TypeVec n` and `Type`.
|
TypeVec.appendFun_comp_splitFun
theorem TypeVec.appendFun_comp_splitFun :
∀ {n : ℕ} {α : TypeVec.{u_1} n} {γ : TypeVec.{u_2} n} {β : Type u_1} {δ : Type u_2} {ε : TypeVec.{u_3} (n + 1)}
(f₀ : ε.drop.Arrow α) (f₁ : α.Arrow γ) (g₀ : ε.last → β) (g₁ : β → δ),
TypeVec.comp (f₁ ::: g₁) (TypeVec.splitFun f₀ g₀) = TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ ∘ g₀)
The theorem `TypeVec.appendFun_comp_splitFun` states that for any natural number `n`, given type vectors `α` and `γ` of length `n`, types `β` and `δ`, and a type vector `ε` of length `n + 1`, if we have type vector arrows `f₀` and `f₁` from the "dropped" version of `ε` to `α` and from `α` to `γ` respectively, as well as functions `g₀` and `g₁` from the "last" type of `ε` to `β` and from `β` to `δ` respectively, then composing the arrow `f₁` with the function `g₁` and then applying it to the result of splitting the functions `f₀` and `g₀` yields the same result as splitting the composition of `f₁` and `f₀` with the composition of `g₁` and `g₀`. In mathematical terms, this asserts the commutativity of certain operations involving type vectors, function composition, and arrow composition in Lean 4.
More concisely: For any natural number `n` and type vectors `α` and `γ` of length `n`, types `β` and `δ`, and type vector arrows `f₀ : ε(0) -> α` and `f₁ : α -> γ`, and functions `g₀ : ε(n) -> β` and `g₁ : β -> δ`, we have `(g₁ ∘ f₁) ∘ (splitFun ε f₀ g₀) = splitFun ε (f₁ ∘ f₀) (g₁ ∘ g₀)`.
|
TypeVec.split_dropFun_lastFun
theorem TypeVec.split_dropFun_lastFun :
∀ {n : ℕ} {α : TypeVec.{u_1} (n + 1)} {α' : TypeVec.{u_2} (n + 1)} (f : α.Arrow α'),
TypeVec.splitFun (TypeVec.dropFun f) (TypeVec.lastFun f) = f
The theorem `TypeVec.split_dropFun_lastFun` states that for any natural number `n`, any two `n+1`-tuples of types `α` and `α'`, and any arrow `f` from `α` to `α'` in the category of `TypeVec`, splitting `f` into a prefix function operating on all but the last element (obtained via `TypeVec.dropFun`) and a function operating on only the last element (obtained via `TypeVec.lastFun`), and then recombining them via `TypeVec.splitFun`, yields the original arrow `f`. Essentially, it verifies that the operations `TypeVec.splitFun`, `TypeVec.dropFun`, and `TypeVec.lastFun` are inverses of each other when used in this manner.
More concisely: For any natural number `n`, any `(α :: TypeVec n)` and `(α' :: TypeVec n)`, and any function `f : α -> α'`, the composition of `TypeVec.splitFun (TypeVec.dropFun f) (TypeVec.lastFun f)` equals `f`.
|