FinVec.map_eq
theorem FinVec.map_eq : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) {m : ℕ} (v : Fin m → α), FinVec.map f v = f ∘ v
The theorem `FinVec.map_eq` states that for any function `f` from a type `α` to a type `β`, and for any function `v` from the finite set `Fin m` to `α`, the application of `f` to each element of `v` (denoted by `FinVec.map f v`) is equivalent to the composition of `f` and `v` (denoted by `f ∘ v`). This theorem can be used, for example, to demonstrate that mapping a function `f : α → β` over the finite vector `![a₁, a₂]` results in `![f a₁, f a₂]`.
More concisely: For any function `f : α -> β` and finite vector `v : Fin m -> α`, `FinVec.map f v` is equal to the composition `f ∘ v`.
|
FinVec.sum_eq
theorem FinVec.sum_eq :
∀ {α : Type u_1} [inst : AddCommMonoid α] {m : ℕ} (a : Fin m → α), FinVec.sum a = Finset.univ.sum fun i => a i := by
sorry
The theorem `FinVec.sum_eq` states that for any type `α` that is an instance of the `AddCommMonoid` class, any natural number `m`, and any function `a` mapping `Fin m` (finite lists of length `m`) to `α`, the sum of the function `a` applied to all elements in the domain (as computed by `FinVec.sum a`) is equal to the sum of the function `a` applied to all elements in the universal finite set (as computed by `Finset.univ.sum fun i => a i`). In other words, it is affirming the equality between two methods of summing over the elements of a finitely-indexed collection.
More concisely: For any `AddCommMonoid α`, function `a` from `Fin m` to `α`, and `m`, the sum of `a` over the universal finite set `Finset.univ` equals the sum of `a` over all elements in `Fin m` (`FinVec.sum a`).
|
FinVec.etaExpand_eq
theorem FinVec.etaExpand_eq : ∀ {α : Type u_1} {m : ℕ} (v : Fin m → α), FinVec.etaExpand v = v
This theorem, `FinVec.etaExpand_eq`, states that for any type `α` and a natural number `m`, for any function `v` from a finite set of size `m` to `α`, the function `FinVec.etaExpand` applied to `v` is equal to `v`. In other words, it asserts the equality between a function and its eta-expanded version, where the function is mapped over an identity function. A notable application of this theorem is that it can be used to prove that a function over a two-element finite set is equivalent to a vector of its function values, as demonstrated in the example.
More concisely: For any type `α` and natural number `m`, the function `FinVec.etaExpand` applied to a function `v` from a finite set of size `m` to `α` equals `v`.
|
FinVec.forall_iff
theorem FinVec.forall_iff :
∀ {α : Type u_1} {m : ℕ} (P : (Fin m → α) → Prop), FinVec.Forall P ↔ ∀ (x : Fin m → α), P x
The theorem `FinVec.forall_iff` establishes a logical equivalence in Lean 4 between two ways of stating a certain universal quantification. Given a type `α`, an integer `m`, and a propositional function `P` that takes a function from `Fin m` to `α`, the theorem states that the proposition `FinVec.Forall P` is logically equivalent to the proposition that `P x` holds for all `x` of type `Fin m → α`. This allows for the expression of the universal quantification in two different but equivalent ways, which can be useful in different proof situations.
More concisely: The theorem `FinVec.forall_iff` in Lean 4 states that the proposition of universal quantification over a function from `Fin m` to `α` is logically equivalent to the proposition that the function maps every element of `Fin m` to a value for which `P` holds.
|
FinVec.exists_iff
theorem FinVec.exists_iff : ∀ {α : Type u_1} {m : ℕ} (P : (Fin m → α) → Prop), FinVec.Exists P ↔ ∃ x, P x
The theorem `FinVec.exists_iff` states that for any type `α` and natural number `m`, and for any predicate `P` that takes a function from finite index set `Fin m` to `α`, the existence of such a function satisfying the predicate `P` is equivalent to the existence of a sequence of `α`-values indexed by `Fin m` satisfying `P`. In simpler terms, it says that there exists a function from `Fin m` to `α` that satisfies `P` if and only if there exists a sequence of elements in `α` that when indexed by `Fin m` also satisfies `P`. This theorem allows us to prove existence of a function in terms of existence of a sequence.
More concisely: For any type `α`, natural number `m`, and predicate `P` on functions from `Fin m` to `α`, the function `P` has a solution if and only if there exists a sequence of length `m` in `α` that satisfies `P`.
|