List.finRange.proof_1
theorem List.finRange.proof_1 : ∀ (n x : ℕ), x ∈ List.range n → x < n
This theorem, identified as `List.finRange.proof_1`, states that for any natural numbers `n` and `x`, if `x` is an element of the list produced by the `List.range` function acting on `n` (i.e., a list of all natural numbers from `0` to `n` exclusive), then `x` is strictly less than `n`. Put in another way, every number in the range from `0` to `n` exclusive is less than `n`.
More concisely: For all natural numbers n and x, if x is in the range 0 to n (exclusive), then x < n.
|
List.nodup_finRange
theorem List.nodup_finRange : ∀ (n : ℕ), (List.finRange n).Nodup
The theorem `List.nodup_finRange` states that for every natural number `n`, the list generated by `List.finRange n` has no duplicates. In other words, each element in the list `List.finRange n`, which comprises all elements of `Fin n` from `0` to `n-1`, appears at most once.
More concisely: For any natural number `n`, the list `List.finRange n` contains no repetitions of elements from `Fin n`.
|
List.nodup_range
theorem List.nodup_range : ∀ (n : ℕ), (List.range n).Nodup
The theorem `List.nodup_range` states that for all natural numbers `n`, the list obtained by the function `List.range n`, which contains the numbers from `0` to `n` exclusive in increasing order, does not contain any duplicate elements. In other words, every element in the list `List.range n` appears at most once.
More concisely: The list generated by `List.range n` is a strictly increasing sequence of length `n+1` without repetitions.
|
List.enum_eq_zip_range
theorem List.enum_eq_zip_range : ∀ {α : Type u} (l : List α), l.enum = (List.range l.length).zip l
This theorem states that for any list `l` of type `α`, the enumeration of `l` (that is, pairing up each element with its index in the list) is equal to zipping the range of the length of `l` (that is, creating a list of numbers from `0` to the length of `l` exclusive) with `l` itself. In other words, the process of enumerating a list of elements is equivalent to pairing each element of the list with its corresponding index from the range of the list's length.
More concisely: For any list `l` of type `α`, the enumeration of `l` is equivalent to zipping `l` with the range `0` to the length of `l`.
|
List.nodup_range'
theorem List.nodup_range' :
∀ (s n : ℕ) (step : optParam ℕ 1), autoParam (0 < step) _auto✝ → (List.range' s n step).Nodup
The theorem `List.nodup_range'` states that for any numbers `s` and `n`, and an optional parameter `step` (which defaults to 1), given that `step` is positive (which is checked automatically), the list produced by the `List.range'` function, which starts at `s` and has `n` steps each of size `step`, contains no duplicate elements.
More concisely: For any integers `s`, `n`, and `step` with `step > 0`, the `List.range` from `s` of length `n` with step `step` contains no repeated elements.
|
List.ranges_length
theorem List.ranges_length : ∀ (l : List ℕ), List.map List.length l.ranges = l
This theorem states that for any list of natural numbers, `l`, when we call `l.ranges` to get a list of lists and then apply `List.length` to each member of this resulting list, we will end up with the original list `l`. In other words, the lengths of the lists produced by `l.ranges` correspond exactly to the natural numbers in `l`.
More concisely: For any list of natural numbers `l`, the lengths of the sublists obtained from `l.ranges` are equal to the numbers in `l`.
|
List.ranges_disjoint
theorem List.ranges_disjoint : ∀ (l : List ℕ), List.Pairwise List.Disjoint l.ranges
This theorem states that for any list of natural numbers `l`, the members of the ranges of `l` are pairwise disjoint. In other words, for each pair of different ranges from the list `l`, there is no common element between them.
More concisely: For any list `l` of natural numbers, the ranges of its elements have no common elements.
|
Mathlib.Data.List.Range._auxLemma.7
theorem Mathlib.Data.List.Range._auxLemma.7 : ∀ {n : ℕ} (a : Fin n), (a ∈ List.finRange n) = True
The theorem `Mathlib.Data.List.Range._auxLemma.7` states that for any natural number `n` and any element `a` of the finite set `Fin n`, `a` is always an element of the list generated by `List.finRange n`. In other words, the function `List.finRange n` generates a list of all elements of the finite set `Fin n` (which contains elements ranging from `0` to `n-1`), and any element `a` from `Fin n` will always be found in this list.
More concisely: For any natural number `n` and element `a` in finite set `Fin n`, `a` is an element of the list generated by `List.finRange n`.
|
List.length_finRange
theorem List.length_finRange : ∀ (n : ℕ), (List.finRange n).length = n
The theorem `List.length_finRange` states that for any natural number `n`, the length of the list of all elements of `Fin n` (generated using the `List.finRange` function) is equal to `n`. Essentially, it means that the list created by `List.finRange` contains `n` elements, where each element is a finite ordinal less than `n`. These finite ordinals range from `0` to `n-1`.
More concisely: The length of the list produced by `List.finRange` over a finite type `Fin n` is equal to `n`.
|
List.ranges_nodup
theorem List.ranges_nodup : ∀ {l s : List ℕ}, s ∈ l.ranges → s.Nodup
This theorem states that, given a list `l` of natural numbers and another list `s` of natural numbers, if `s` is in the range of `l`, then `s` does not contain any duplicate elements. In other words, all members of the ranges of a list of natural numbers are guaranteed to be lists without any repeating elements.
More concisely: If a list `l` of natural numbers is the range of another list `s` of natural numbers, then `s` has no repeating elements.
|