Pi.single_eq_of_ne'
theorem Pi.single_eq_of_ne' :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] {i i' : I},
i ≠ i' → ∀ (x : f i), Pi.single i x i' = 0
This theorem, `Pi.single_eq_of_ne'`, states that for any type `I`, a function `f` from `I` to some type `v₁`, given that equality is decidable on `I` and for every `i` in `I` there exists a zero in `f i`, if `i` is not equal to `i'`, then for any `x` from `f i`, the function `Pi.single i x i'` is equal to zero. In simpler words, this theorem asserts that for a function defined at a specific point `i` with value `x` and `0` elsewhere, if we evaluate this function at a different point `i'`, the value will be `0`.
More concisely: Given a function from type `I` to some type, if equality is decidable on `I` and for every `i ≠ i'` in `I`, there exists a zero in the function's value at `i`, then for all `x` in the function's value at `i`, the function's value at `i'` is equal to zero.
|
Pi.add_apply
theorem Pi.add_apply :
∀ {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [inst : (i : I) → Add (f i)],
(x + y) i = x i + y i
This theorem, `Pi.add_apply`, states that for any type `I`, for any function `f` mapping `I` to another type `v₁`, and for any two mappings `x` and `y` from `I` to `f`, and for any element `i` of `I`, if a `Add` instance is defined for `f i`, then applying the `+` operator to `x` and `y` and then applying the result to `i` is the same as applying `x` and `y` to `i` and then adding the results. In other words, it shows that addition in the context of these types of functions satisfies the property of distributivity over function application.
More concisely: For any type `I`, function `f : I -> v₁`, and elements `x, y : I -> f`, if `I` has an `Add` instance and `i : I`, then `(x + y) i = x i + y i`.
|
Pi.single_comm
theorem Pi.single_comm :
∀ {I : Type u} {β : Type u_2} [inst : DecidableEq I] [inst_1 : Zero β] (i : I) (x : β) (i' : I),
Pi.single i x i' = Pi.single i' x i
The theorem `Pi.single_comm` states that for any non-dependent functions, the `Pi.single` function, which creates a function with value `x` at index `i` and `0` elsewhere, is symmetric in its two indices. This means for any types `I` and `β`, given decidable equality on `I` and a zero element in `β`, and for any elements `i`, `x` and `i'` of `I`, `β` and `I` respectively, applying `Pi.single` to `i`, `x` and then `i'` will yield the same result as applying `Pi.single` to `i'`, `x` and then `i`.
More concisely: For any type `I` with decidable equality, and for any non-dependent functions `f : I -> β`, `Pi.single f i = Pi.single f i'` holds for all `i, i' in I` and `x in β`.
|
Pi.mulSingle_eq_same
theorem Pi.mulSingle_eq_same :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → One (f i)] (i : I) (x : f i),
Pi.mulSingle i x i = x
The theorem `Pi.mulSingle_eq_same` states that for any index set `I` and a function `f` from `I` to another type, whenever we have a decidable equality on the index set `I` and an identity element (which we call `One`) for each element in the range of `f`, for any specific index `i` in `I` and value `x` of the type `f i`, the value at index `i` of the function `Pi.mulSingle i x`, which creates a function that is `1` everywhere except at `i` where it is `x`, is indeed `x`. In essence, it shows that `Pi.mulSingle` correctly assigns the value `x` at the specified index `i`.
More concisely: For any decidable equality relation on an index set `I`, function `f` from `I` to a type with identity elements `One` in its range, and index `i` in `I` and value `x` of type `f i`, `Pi.mulSingle i x` equals `x` as functions.
|
Pi.mulSingle_apply
theorem Pi.mulSingle_apply :
∀ {I : Type u} {β : Type u_2} [inst : DecidableEq I] [inst_1 : One β] (i : I) (x : β) (i' : I),
Pi.mulSingle i x i' = if i' = i then x else 1
This theorem states that for non-dependent functions, the value of `Pi.mulSingle` at a particular index `i'` can be expressed using an "if-then-else" condition. Specifically, if the given index `i'` equals `i`, then `Pi.mulSingle i x i'` equals `x`. If `i'` does not equal `i`, then `Pi.mulSingle i x i'` equals `1`. Here, `I` is the type of the index, `β` is the value type, `i` is the index where the function has the value `x`, and `i'` is the index of interest. `Pi.mulSingle` is a function which takes an index and a value, and produces a function which takes another index and gives the value if the indices match, or `1` otherwise.
More concisely: For non-dependent functions `Pi` of type `I -> β`, the expression `Pi.mulSingle i x i'` equals `x` if `i = i'`, and equals `1` otherwise.
|
Pi.single_eq_same
theorem Pi.single_eq_same :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] (i : I) (x : f i),
Pi.single i x i = x
The theorem `Pi.single_eq_same` states that for any type `I` and a type-valued function `f` on `I`, given that `I` has decidable equality and each type `f i` for `i` in `I` has a defined zero, for any element `i` of `I` and an element `x` of type `f i`, the function `Pi.single i x` evaluated at `i` is equal to `x`. In other words, if we define a function using `Pi.single` where the function is supposed to be `x` at index `i` and zero elsewhere, then indeed, the function's value at `i` is `x`.
More concisely: For any type `I` with decidable equality, and a function `f` from `I` to a type with defined zero for each `i`, the element-wise application of `Pi.single i x` and `x` coincides for all `i` in `I`.
|
Pi.single_op
theorem Pi.single_op :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] {g : I → Type u_4}
[inst_2 : (i : I) → Zero (g i)] (op : (i : I) → f i → g i),
(∀ (i : I), op i 0 = 0) → ∀ (i : I) (x : f i), Pi.single i (op i x) = fun j => op j (Pi.single i x j)
This theorem, `Pi.single_op`, states that for any type `I`, any function `f` from `I` to a type, any function `g` from `I` to a type, under the assumption that `I` has decidable equality and each type that `f` and `g` maps to has a zero value, given an operator `op` which operates on each element of `I` and its corresponding value under `f` to produce a value of type under `g`. If this operator applied to any element of `I` and zero gives zero, then for all elements `i` of `I` and all `x` in the image of `f`, the function supported at `i` with value `op i x` there, and `0` elsewhere, equals to the function which maps each element `j` of `I` to `op j` applied to the function supported at `i` with value `x` there, and `0` elsewhere. In other words, the operator `op` can be distributed over the function supported at a single point.
More concisely: If `I` is a decidably equal type, `f: I -> T`, `g: I -> U`, `op: I -> T -> U`, and for all `i` in `I` and `x` in `Imap f`, `op i x = op i 0`, then for all `i` in `I` and `x` in `Imap f`, `op i x = (op i) . (map (const x) . pointwise (const i) . f) 0`.
|
Pi.single_zero
theorem Pi.single_zero :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] (i : I),
Pi.single i 0 = 0
This theorem, `Pi.single_zero`, states that for any type `I`, any function `f` that maps elements of `I` to some type, and any element `i` of `I`, if we have decidable equality on `I` and each `f i` is an additive identity (i.e., zero), then the function `Pi.single i 0` is equivalent to the zero function. In simpler terms, it says that if we create a function that takes value `0` at `i` and `0` elsewhere, that function is equivalent to a function that takes value `0` everywhere.
More concisely: If `I` is a type with decidable equality, `f : I → T`, and `i ∈ I` such that `f i` is the additive identity in `T` for all `i ∈ I`, then `Pi.single i 0` equals the zero function `0 : I → T`.
|
Pi.single_apply
theorem Pi.single_apply :
∀ {I : Type u} {β : Type u_2} [inst : DecidableEq I] [inst_1 : Zero β] (i : I) (x : β) (i' : I),
Pi.single i x i' = if i' = i then x else 0
The theorem `Pi.single_apply` states that for any given types `I` and `β`, with `I` having a decidable equality operation and `β` having a zero element, and for any elements `i` and `i'` of `I` and any element `x` of `β`, the value of the function `Pi.single` at index `i'` is `x` if `i'` is equal to `i` and is `0` otherwise. In other words, `Pi.single` generates a function that maps `i` to `x` and all other indices to `0`, behaving similar to an `if-then-else` construct.
More concisely: For any types `I` with decidable equality and having a zero element `β`, the function `Pi.single` maps index `i'` to element `x` if `i'` equals `i`, and to zero otherwise.
|
Pi.single_eq_of_ne
theorem Pi.single_eq_of_ne :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] {i i' : I},
i' ≠ i → ∀ (x : f i), Pi.single i x i' = 0
The theorem `Pi.single_eq_of_ne` states that for any type `I`, a function `f : I → Type v₁`, an instance of decidable equality on `I`, and an instance of zero for `f i`, if `i'` and `i` are distinct (i.e., `i' ≠ i`), then for any `x` in the codomain of `f` at `i`, the value of the function `Pi.single i x` at `i'` is zero. In other words, it asserts that the "single" function, which assigns the value `x` to `i` and zero to all other elements of `I`, indeed returns zero for inputs not equal to `i`.
More concisely: For any function `f : I -> Type v₁`, decidable equality on `I`, and `i ≠ i'` in `I`, the "single" function `Pi.single i x` assigns zero to `i'` for any `x` in the codomain of `f`.
|
Pi.neg_apply
theorem Pi.neg_apply :
∀ {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [inst : (i : I) → Neg (f i)], (-x) i = -x i
This theorem, `Pi.neg_apply`, states that for any type `I` and any function `f : I → Type v₁`, given a dependent function `x : (i : I) → f i` and an index `i : I`, if every `f i` has a negation operation, then applying the negation to the function `x` at index `i` is the same as the negation of the value of the function `x` at index `i`. In other words, negating the function before applying it gives the same result as applying it first and then negating the outcome.
More concisely: For any type `I` and function `f : I → Type v₁`, if `i : I` is an index such that each `f i` has a negation operation, then `neg (x i) = neg (f i x i)`.
|
Pi.mulSingle_one
theorem Pi.mulSingle_one :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → One (f i)] (i : I),
Pi.mulSingle i 1 = 1
This theorem states that for any type `I`, and any function `f` which maps elements of `I` to a type, given that equality is decidable on `I` and that all types `f i` for `i` in `I` have a multiplicative identity, for any element `i` of `I`, the function `Pi.mulSingle` applied to `i` and the multiplicative identity of `f i` is equivalent to the multiplicative identity function. In simpler terms, if you have a function that's like a vector of 1s, and you replace one of the entries with 1, you still have the same vector of 1s.
More concisely: For any type `I` with decidable equality and each function `f : I →* X` from `I` to a type `X` with identity element `one_x : X`, the function `Pi.mulSingle : I → X → X` satisfies `Pi.mulSingle i one_x = one_x` for all `i : I`.
|
Pi.mulSingle_comm
theorem Pi.mulSingle_comm :
∀ {I : Type u} {β : Type u_2} [inst : DecidableEq I] [inst_1 : One β] (i : I) (x : β) (i' : I),
Pi.mulSingle i x i' = Pi.mulSingle i' x i
The theorem `Pi.mulSingle_comm` states that for any types `I` and `β` where `I` supports decidable equality and `β` has a defined `One` instance, the `Pi.mulSingle` function, which maps an element of `I` to a corresponding element of `β`, is symmetric in its two indices. In other words, for any specific elements `i`, `x` and `i'` from `I`, `β` and `I` respectively, applying `Pi.mulSingle` to `i` and `x` first and then to `i'` is equivalent to applying `Pi.mulSingle` to `i'` and `x` first and then to `i`.
More concisely: For types `I` with decidable equality and `β` having a `One` instance, the function `Pi.mulSingle : I → β → β` is commutative, i.e., `Pi.mulSingle i x = Pi.mulSingle i' x ↔ Pi.mulSingle i' x = Pi.mulSingle i x`.
|
Pi.mulSingle_eq_of_ne'
theorem Pi.mulSingle_eq_of_ne' :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → One (f i)] {i i' : I},
i ≠ i' → ∀ (x : f i), Pi.mulSingle i x i' = 1
This theorem, `Pi.mulSingle_eq_of_ne'`, states that for any types `I` and `f` such that `f` is a function from `I` to some other type, given a decidable equality on `I` and a function that assigns a 'one' value to each element of `I`, if we have two distinct elements `i` and `i'` of `I`, then the function `Pi.mulSingle` applied to `i`, a value `x` of type `f i`, and `i'` will always return `1`. Essentially, it says that for any 'non-diagonal' element of a function defined by `Pi.mulSingle`, the value is `1`.
More concisely: Given a type `I`, a decidable equality relation on `I`, a function `f : I →* X`, and distinct elements `i ≠ i'` of `I`, `Pi.mulSingle i x i' = 1`.
|
Pi.mul_apply
theorem Pi.mul_apply :
∀ {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [inst : (i : I) → Mul (f i)],
(x * y) i = x i * y i
This theorem states that for any type `I` and a function `f` mapping `I` to another type `v₁`, given two functions `x` and `y` from `I` to `f i` and an element `i` of type `I`, and assuming that a multiplication operation is defined for each `f i`, the result of multiplying the functions `x` and `y` (i.e., `(x * y)`) applied to `i` is equal to the result of multiplying the values of `x i` and `y i`. In other words, it formalizes the property of point-wise multiplication of functions.
More concisely: For any type `I` and function `f : I -> Type`, given functions `x, y : I -> f i`, and an element `i : I` with a defined multiplication operation on `f i`, we have `(x * y) i = x i * y i`.
|
Pi.apply_single
theorem Pi.apply_single :
∀ {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)]
[inst_2 : (i : I) → Zero (g i)] (f' : (i : I) → f i → g i),
(∀ (i : I), f' i 0 = 0) → ∀ (i : I) (x : f i) (j : I), f' j (Pi.single i x j) = Pi.single i (f' i x) j
This theorem, `Pi.apply_single`, states that for any types `I`, `f`, and `g`, given a function `f'` that maps elements of type `f` to type `g` for each element in `I`, and assuming that `f' i 0` is always `0` for all `i` in `I`, the application of `f'` on `Pi.single i x j` (i.e., a function that is `0` everywhere except at `i` where it is `x`) is equal to `Pi.single i (f' i x) j`. In other words, under these conditions, applying `f'` to the function supported at `i` does not change its support. This theorem is a generalization of the property of sparse functions where applying a function to a sparse vector preserves its sparsity.
More concisely: For any types `I`, `f`, and `g`, if `f' : I → g` is a function such that `f' i 0 = 0` for all `i` in `I`, then `f' (Pi.single i x) = Pi.single i (f' i x)` for all `i` in `I` and `x : f`.
|
Pi.single_injective
theorem Pi.single_injective :
∀ {I : Type u} (f : I → Type v₁) [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] (i : I),
Function.Injective (Pi.single i)
This theorem states that for any type `I`, any type-valued function `f` on `I`, any element `i` of `I`, and given that the elements of `f(i)` have a zero and that `I` has decidable equality, then the function `Pi.single i`, which creates a function from `I` to `f(j)` that is zero everywhere except at `i`, where it has a specified value, is injective. In other words, if `Pi.single i x = Pi.single i y` then `x = y`. Injective refers to the property that different inputs will produce different outputs, so no two different values `x` and `y` from `f(i)` can produce the same function when applied to `Pi.single i`.
More concisely: For any type `I`, function `f` on `I` with decidable equality, and `i` in `I` such that `f(i)` has a zero, the function `Pi.single i : I -> f i` is an injective function.
|
Pi.zero_apply
theorem Pi.zero_apply : ∀ {I : Type u} {f : I → Type v₁} (i : I) [inst : (i : I) → Zero (f i)], 0 i = 0
This theorem, `Pi.zero_apply`, states that for any type `I`, any function `f` mapping elements of `I` to some other type, and any element `i` of `I`, if each `f i` is equipped with a zero element, then applying the zero function to `i` results in the zero of `f i`. In mathematical terms, if we have a function `f` from `I` to some other type such that each `f(i)` has a zero, then the zero at `f(i)` is the same as the zero element of `f(i)`.
More concisely: For any type `I` and function `f` from `I` to a type with zero elements, the application of the zero function to an element `i` of `I` results in the zero of `f i`. In other words, `zero_apply f i = f i zero`.
|
Pi.prod_fst_snd
theorem Pi.prod_fst_snd : ∀ {α : Type u_1} {β : Type u_2}, Pi.prod Prod.fst Prod.snd = id
This theorem, `Pi.prod_fst_snd`, states that for all types `α` and `β`, the product mapping of the first and second projections (`Prod.fst` and `Prod.snd`) is the identity function. In simpler terms, when you create a pair by collecting the results of applying the first and second projection functions (which essentially deconstruct a pair into its two components) and then apply this operation to any pair, you would get the original pair back. It shows the compatibility of the product mapping with the projection operations in the context of pair-type data.
More concisely: For all types `α` and `β`, the function that maps a pair `(a, b)` to `(Prod.fst (a, b), Prod.snd (a, b))` is the identity function on pairs of type `(α × β)`.
|
Pi.mulSingle_eq_of_ne
theorem Pi.mulSingle_eq_of_ne :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → One (f i)] {i i' : I},
i' ≠ i → ∀ (x : f i), Pi.mulSingle i x i' = 1
The theorem `Pi.mulSingle_eq_of_ne` states that for any types `I` and `f`, where `f` is a function from `I` to some type, and given instances of decidable equality for `I` and of the multiplicative identity for `f i` for all `i` in `I`, if `i'` and `i` are distinct elements of `I`, then the function `Pi.mulSingle` evaluated at `i'` is equal to `1` for any `x` in the range of `f` at `i`. In other words, for different indexes `i` and `i'`, the function `Pi.mulSingle` returns the multiplicative identity when evaluated at `i'`.
More concisely: For any function `f` from a decidably equal type `I` to some type, if instances of decidable equality for `I` and multiplicative identity for `f i` exist for all `i` in `I`, then `Pi.mulSingle f i'` equals the multiplicative identity for all distinct `i'` and `i` in `I`.
|
Pi.one_apply
theorem Pi.one_apply : ∀ {I : Type u} {f : I → Type v₁} (i : I) [inst : (i : I) → One (f i)], 1 i = 1
This theorem, `Pi.one_apply`, states that for any type `I` and any function `f` from `I` to another type `v₁`, given any element `i` of `I` and assuming that for each `i` in `I` the type `f i` has a multiplicative identity (i.e., it has a `One` instance), applying the multiplicative identity `1` to `i` is the same as the multiplicative identity `1` itself. In simple terms, it says that the identity element does not change when applied to an element of the domain.
More concisely: For any type `I` and function `f` from `I` to a type with a multiplicative identity, the application of the multiplicative identity `1` to an element `i` of `I` equals the identity `1` itself.
|
Pi.sub_apply
theorem Pi.sub_apply :
∀ {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [inst : (i : I) → Sub (f i)],
(x - y) i = x i - y i
This theorem states that for any type `I` and a function `f` mapping `I` to another type `v₁`, given two function instances `x` and `y` (which map `I` to `f i`), and a particular index `i` from `I`, if subtraction is defined on the type `f i`, then the subtraction of `x` and `y` evaluated at `i` is the same as the subtraction of the evaluations of `x` and `y` at `i`. In other words, we can distribute the application of a function over subtraction, similar to how we can distribute multiplication over addition in basic algebra.
More concisely: For any type `I` and function `f : I → v₁`, if `i ∈ I` has defined subtraction `(v₁ : Type)`, then `(x - y) i = x i - y i`, where `x`, `y : I → f`.
|
Pi.smul_apply
theorem Pi.smul_apply :
∀ {I : Type u} {β : Type u_2} {f : I → Type v₁} [inst : (i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) (i : I),
(b • x) i = b • x i
This theorem states that for any index set `I`, any type `β`, and any function `f` from `I` to some type `v₁`, given a scalar multiplication instance on `(f i)` for each `i` in `I`, a scalar `b` of type `β`, and a function `x` from `I` to `f i`, the result of scalar multiplication applied to `x` at a particular index `i` is the same as scalar multiplying the result of `x` evaluated at `i`. Essentially, it is the formalization of the rule of distribution of scalar multiplication over a function in a product space.
More concisely: For any index set `I`, type `β`, function `f` from `I` to some type `v₁`, scalar multiplication instance on `(f i)` for each `i` in `I`, scalar `b` of type `β`, and function `x` from `I` to `f i`, we have `b * (x i) = x i * b`.
|
Pi.single_op₂
theorem Pi.single_op₂ :
∀ {I : Type u} {f : I → Type v₁} [inst : DecidableEq I] [inst_1 : (i : I) → Zero (f i)] {g₁ : I → Type u_4}
{g₂ : I → Type u_5} [inst_2 : (i : I) → Zero (g₁ i)] [inst_3 : (i : I) → Zero (g₂ i)]
(op : (i : I) → g₁ i → g₂ i → f i),
(∀ (i : I), op i 0 0 = 0) →
∀ (i : I) (x₁ : g₁ i) (x₂ : g₂ i),
Pi.single i (op i x₁ x₂) = fun j => op j (Pi.single i x₁ j) (Pi.single i x₂ j)
This theorem is known as `Pi.single_op₂`. It states that for any type `I`, and for any type functions `f`, `g₁`, and `g₂` from `I` to some other types, given that `I` has a decidable equality, and `f`, `g₁`, and `g₂` are equipped with a zero element at each `i : I`, if we have a binary operation `op : (i: I) → g₁ i → g₂ i → f i` such that `op i 0 0 = 0` for all `i : I`, then for each `i : I` and elements `x₁ : g₁ i` and `x₂ : g₂ i`, the function `Pi.single i (op i x₁ x₂)` equals the function that takes any `j : I` and maps it to `op j (Pi.single i x₁ j) (Pi.single i x₂ j)`. This theorem essentially asserts a property related to the interaction between a certain binary operation and the function `Pi.single`, which gives the value `x` at `i` and `0` elsewhere.
More concisely: For any type `I` with decidable equality, functions `f, g₁, g₂ : I →* X` from `I` to some type `X`, and a binary operation `op : I → g₁ → g₂ → f`, if `op` satisfies `op i 0 0 = 0` for all `i : I`, then `Pi.single i (op i ( Pi.single i x₁ i ) ( Pi.single i x₂ i )) = λ j, op j (Pi.single i x₁ j) (Pi.single i x₂ j)` for all `x₁ : g₁ i` and `x₂ : g₂ i`.
|