List.ofFn_inj'
theorem List.ofFn_inj' :
∀ {α : Type u} {m n : ℕ} {f : Fin m → α} {g : Fin n → α}, List.ofFn f = List.ofFn g ↔ ⟨m, f⟩ = ⟨n, g⟩
The theorem `List.ofFn_inj'` states that for any type `α` and natural numbers `m` and `n`, and functions `f : Fin m → α` and `g : Fin n → α`, the list generated by applying `f` to each value from `0` to `m - 1` is equal to the list generated by applying `g` to each value from `0` to `n - 1` if and only if the pair consisting of `m` and `f` is equal to the pair consisting of `n` and `g`. This theorem may be useful when working with the right-hand side of expressions involving `Fin.sigma_eq_iff_eq_comp_cast`.
More concisely: For functions `f : Fin m -> α` and `g : Fin n -> α`, the lists `[f 0 : list α | i in Fin.range m]` and `[g 0 : list α | i in Fin.range n]` are equal if and only if `m = n` and `f = g`.
|
List.mem_ofFn
theorem List.mem_ofFn : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (a : α), a ∈ List.ofFn f ↔ a ∈ Set.range f
This theorem, `List.mem_ofFn`, states that for any type `α`, any natural number `n`, any function `f` from the finite set `Fin n` to `α`, and any element `a` of type `α`, `a` belongs to the list generated by applying `f` to each element in `Fin n` if and only if `a` belongs to the range of `f`. In other words, an element is in the list produced by a function when it is applied to the finite set if and only if it is in the set of values that the function can produce.
More concisely: For any type `α`, natural number `n`, function `f` from `Fin n` to `α`, and `a` in `α`, `a` is in the list `[f x | x ∈ Fin n]` if and only if `a` is in the range of `f`.
|
List.map_ofFn
theorem List.map_ofFn :
∀ {α : Type u} {β : Type u_1} {n : ℕ} (f : Fin n → α) (g : α → β), List.map g (List.ofFn f) = List.ofFn (g ∘ f)
This theorem states that for any types `α` and `β`, any natural number `n`, any function `f` from `Fin n` to `α`, and any function `g` from `α` to `β`, the result of mapping `g` over the list produced by applying `f` to each element in the finite sequence from 0 to `n - 1` (expressed as `List.ofFn f`) is the same as the list produced by applying the composition of `g` and `f` to each element in the same finite sequence (expressed as `List.ofFn (g ∘ f)`). In other words, mapping a function over the list obtained by applying a function to a sequence is the same as applying the composition of the two functions to the sequence.
More concisely: For any types `α` and `β`, any function `f : Fin n → α`, and any function `g : α → β`, `List.ofFn (g ∘ f) = List.map g (List.ofFn f)`.
|
List.ofFn_const
theorem List.ofFn_const : ∀ {α : Type u} (n : ℕ) (c : α), (List.ofFn fun x => c) = List.replicate n c
The theorem `List.ofFn_const` states that for any type `α`, any natural number `n`, and any constant `c` of type `α`, creating a list by applying a function that always returns `c` on `Fin n` (which essentially represents the first `n` natural numbers) is the same as creating a list by replicating `c` `n` times. In other words, the list containing `n` elements, all of which are `c`, can be created either by applying a constant function to the first `n` natural numbers, or by directly replicating `c` `n` times.
More concisely: For any type `α` and natural number `n`, the function application `map (const c) ( Fin.range n )` equals the list `replicate n c`.
|
List.ofFn_zero
theorem List.ofFn_zero : ∀ {α : Type u} (f : Fin 0 → α), List.ofFn f = []
The theorem `List.ofFn_zero` states that when the function `ofFn` is applied on an empty domain, it results in an empty list. In more detail, for any type `α` and any function `f` from the finite set of size 0 to `α`, the list obtained by applying `f` to each element in the domain (in this case there are no elements as the domain is empty) is an empty list.
More concisely: For any function from the empty set to type α, the application of `ofFn` results in an empty list.
|
List.ofFn_mul'
theorem List.ofFn_mul' :
∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨m * ↑i + ↑j, ⋯⟩).join
This theorem states that for any type `α` and any natural numbers `m` and `n`, for any function `f` mapping from a finite set of `m * n` elements to `α`, the list generated by applying `f` to each element in the finite set can be broken down into `n` sublists, each having `m` elements. This is done by first creating `n` sublists using `f` where each sublist is created with `m` elements, and then joining these sublists. The original list and the joined list are equal.
More concisely: For any function `f` and finite sets `X` of size `m * n`, the image `f` of `X` can be partitioned into `n` sublists `[f x | x ∈ S]` for each `S ⊆ X` of size `m`, such that the concatenation of these sublists is equal to the image of `X` under `f`.
|
List.ofFn_get
theorem List.ofFn_get : ∀ {α : Type u} (l : List α), List.ofFn l.get = l
This theorem states that for any list `l` of elements of some type `α`, if we build a new list using the function `List.ofFn` with `List.get l` as its argument (a function that retrieves the element at a given index in `l`), the new list will be identical to the original list `l`. In other words, retrieving each element from the list `l` in order and constructing a new list from those elements results in a list that is the same as `l`. It's essentially saying that the `List.ofFn` function with `List.get l` as its argument is a way to clone or copy a list.
More concisely: For any list `l` of type `α`, the list obtained by applying `List.ofFn` with `List.get` on `l` is equal to the original list `l`. In other words, `List.ofFn (λ (i, x) := List.get i l) = l`.
|
List.ofFn_injective
theorem List.ofFn_injective : ∀ {α : Type u} {n : ℕ}, Function.Injective List.ofFn
This theorem, `List.ofFn_injective`, asserts that for every type `α` and natural number `n`, the function `List.ofFn` is injective. In other words, if we have two functions `f` and `g` from `Fin n → α` such that `List.ofFn f = List.ofFn g`, it must be the case that `f = g`. This means that creating lists from functions using `List.ofFn` preserves the uniqueness of the functions: no two different functions will produce the same list.
More concisely: For all types `α` and natural numbers `n`, the function `List.ofFn : ∀ (f g : Fin n → α), (List.ofFn f = List.ofFn g) ↔ f = g` is a propositional equality that is an equivalence.
|
List.length_ofFn
theorem List.length_ofFn : ∀ {α : Type u} {n : ℕ} (f : Fin n → α), (List.ofFn f).length = n
This theorem states that for any function `f` from the finite set `Fin n` to any type `α`, the length of the list created by applying `f` to each element in `Fin n` (using `List.ofFn`) is equal to `n`. In other words, when a function `f` is mapped over a finite domain `Fin n` to generate a list, the size (length) of the resulting list will be the same as the size of the domain `n`.
More concisely: For any function from a finite set `Fin n` to type `α`, the length of the list obtained by applying `List.ofFn` is equal to `n`.
|
List.ofFn_inj
theorem List.ofFn_inj : ∀ {α : Type u} {n : ℕ} {f g : Fin n → α}, List.ofFn f = List.ofFn g ↔ f = g
The theorem `List.ofFn_inj` states that for any type `α`, any natural number `n`, and any two functions `f` and `g` from `Fin n` to `α`, the list constructed by applying `List.ofFn` to `f` is equal to the list constructed by applying `List.ofFn` to `g` if and only if `f` is equal to `g`. In other words, two functions `f` and `g` produce the same list when passed to `List.ofFn` if and only if they are the same function.
More concisely: For any type `α` and natural number `n`, the functions `List.ofFn f` and `List.ofFn g` from `Fin n` to `List α` agree if and only if functions `f` and `g` from `Fin n` to `α` are equal.
|
List.ofFn_mul
theorem List.ofFn_mul :
∀ {α : Type u} {m n : ℕ} (f : Fin (m * n) → α),
List.ofFn f = (List.ofFn fun i => List.ofFn fun j => f ⟨↑i * n + ↑j, ⋯⟩).join
The theorem `List.ofFn_mul` states that for any type `α`, and for any natural numbers `m` and `n`, given a function `f` that maps from the finite set of size `m * n` to `α`, the list generated by applying `f` can be broken down into `m` sublists each containing `n` elements. This is accomplished by first creating a list where each element is itself a list generated from `f`, and then joining these lists together. This provides a way to transform a single list into a grouped structure.
More concisely: Given a function `f` mapping a finite set of size `m * n` to type `α`, there exists a list `ls` of `m` sublists, each of length `n`, such that `ls` is equivalent to the list obtained by applying `f` to the elements of the finite set.
|
List.get?_ofFn
theorem List.get?_ofFn : ∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : ℕ), (List.ofFn f).get? i = List.ofFnNthVal f i
The theorem `List.get?_ofFn` states that for any type `α`, any natural number `n`, any function `f` from `Fin n` to `α`, and any natural number `i`, the `i`th element of the list generated by applying `f` to each element of `Fin n` is equal to the result of applying the function `List.ofFnNthVal` to `f` and `i`. This means that pulling the `i`th element from the created list directly or using `List.ofFnNthVal` gives the same result. If `i` is less than `n`, both methods will return `some (f i)`, and if `i` is greater or equal to `n`, both will return `none`.
More concisely: For any type α, natural number n, function f : Fin n → α, and natural number i, List.get?(List.ofFn n f) i = List.ofFnNthVal f i.
|
List.get_ofFn
theorem List.get_ofFn :
∀ {α : Type u} {n : ℕ} (f : Fin n → α) (i : Fin (List.ofFn f).length), (List.ofFn f).get i = f (Fin.cast ⋯ i) := by
sorry
This theorem, `List.get_ofFn`, states that for any type `α` and positive integer `n`, given a function `f` from the finite set `Fin n` to `α` and an index `i` within the length of the list created by the function `List.ofFn f`, the element at index `i` in the `List.ofFn f` is the same as the result of the function `f` applied to `i` cast into the same `Fin` type. In other words, this theorem guarantees that the `List.ofFn` function correctly generates a list by applying function `f` to each element in the finite set `Fin n`.
More concisely: For any type `α` and positive integer `n`, the element at index `i` in the list `List.ofFn f` equals `f` applied to the index `i` considered as a finite number in `Fin n`.
|
List.ofFn_succ
theorem List.ofFn_succ :
∀ {α : Type u} {n : ℕ} (f : Fin n.succ → α), List.ofFn f = f 0 :: List.ofFn fun i => f i.succ
The theorem `List.ofFn_succ` states that for any given type `α`, natural number `n`, and function `f` from `Fin (Nat.succ n)` to `α`, creating a list of function's results via `List.ofFn f` is equivalent to having the first element as `f 0` and the rest of the list generated by applying `f` to the successor of each `i` in `Fin n`. In other words, it states that the list generated by applying `f` to each element in `Fin (Nat.succ n)` is the same as the list obtained by prepending `f 0` to the list generated by applying `f` to the successor of each element in `Fin n`.
More concisely: For any type `α`, natural number `n`, and function `f` from `Fin (Nat.succ n)` to `α`, the list `[f 0 :: List.map succ (List.map f (Fin.range n))]` equals `List.ofFn f (Fin.range (Nat.succ n))`.
|
List.ofFn_add
theorem List.ofFn_add :
∀ {α : Type u} {m n : ℕ} (f : Fin (m + n) → α),
List.ofFn f = (List.ofFn fun i => f (Fin.castAdd n i)) ++ List.ofFn fun j => f (Fin.natAdd m j)
The theorem `List.ofFn_add` states that for any type `α` and any two natural numbers `m` and `n`, and any function `f` mapping from the finite set of `m + n` elements to `α`, creating a list from `f` using `List.ofFn` is equivalent to creating two lists: the first one is created by applying `f` to `Fin.castAdd n i` for each `i` (which embeds `i` from `Fin m` into `Fin (m + n)`), and the second one is created by applying `f` to `Fin.natAdd m j` for each `j` (which adds `m` to `j` "on the left"). These two lists are then concatenated together. This matches the convention of `List.ofFn_succ'`, where the elements from `Fin m` are put first.
More concisely: For any type `α` and functions `f` mapping from a finite set of `m + n` elements to `α`, `List.ofFn (f : Fin (m + n) -> α) = List.map (Fin.castAdd n) (List.range m) ++ List.map (Fin.natAdd m) (List.range n)`.
|