List.sublist_join
theorem List.sublist_join : ∀ {α : Type u_1} (L : List (List α)) {s : List α}, s ∈ L → s.Sublist L.join
This theorem, `List.sublist_join`, states that for any list of lists `L` of any type `α`, and for any list `s` of type `α`, if `s` is a member of `L`, then `s` is a sublist of the joined version of `L`. In other words, any element of a list of lists is guaranteed to be a sublist of the concatenation of all the lists in `L`.
More concisely: For any list `L` of lists `α` and any list `s` of type `α`, if `s` is an element of `L`, then `s` is a sublist of the concatenation of `L`.
|
List.reverse_join
theorem List.reverse_join :
∀ {α : Type u_1} (L : List (List α)), L.join.reverse = (List.map List.reverse L).reverse.join
The theorem `List.reverse_join` states that for any list of lists `L` of type `α`, reversing the joined list `L` is equivalent to first reversing each inner list of `L`, then reversing the order of the resulting list of lists, and finally joining this list. In other words, the reverse of the concatenation of a sequence of lists is the same as concatenating the reversed sequence of the reversed lists.
More concisely: For any list of lists `L` of type `α`, the concatenation of the reversed lists in the reversed order is equal to the reverse of the concatenation of the original lists.
|
List.eq_iff_join_eq
theorem List.eq_iff_join_eq :
∀ {α : Type u_1} (L L' : List (List α)),
L = L' ↔ L.join = L'.join ∧ List.map List.length L = List.map List.length L'
This theorem asserts that, for any two lists of lists (`L` and `L'`) over any type `α`, the two lists are equal if and only if two conditions are met: First, the joined versions of these lists are equal (i.e., when all the sublists are concatenated together, the resulting lists are the same). Second, the lengths of their corresponding sublists are equal when mapped as separate lists (i.e., the lists of lengths of the sublists in the same order are identical).
More concisely: Two lists of lists over type `α`, `L` and `L'`, are equal if and only if their concatenated sublists are equal and their corresponding length lists are equal.
|
List.join_reverse
theorem List.join_reverse :
∀ {α : Type u_1} (L : List (List α)), L.reverse.join = (List.map List.reverse L).join.reverse
This theorem states that for any list of lists `L` of a certain type `α`, reversing `L` and then joining the resulting lists is equivalent to first reversing all the sublists of `L`, joining them, and then reversing the result. This theorem essentially describes a property of list transformation operations in Lean 4.
More concisely: For any list of lists `L` of type `α`, the concatenation of the reversed sublists of `L` and their reversal is equivalent to the reverse of the concatenation of `L`.
|
List.append_join_map_append
theorem List.append_join_map_append :
∀ {α : Type u_1} (L : List (List α)) (x : List α),
x ++ (List.map (fun x_1 => x_1 ++ x) L).join = (List.map (fun x_1 => x ++ x_1) L).join ++ x
This theorem states that for any list `L` of lists and any list `x`, both of type `α`, we can rearrange the brackets in a series of list concatenations. Specifically, if we start with the list `x` followed by the concatenation of each list in `L` appended with `x`, all joined together, it is equivalent to joining together each list in `L` prepended with `x`, and then appending `x` at the end. Symbolically, it's saying that `x ++ (l₁ ++ x) ++ (l₂ ++ x) ++ ... ++ (lₙ ++ x)` is equivalent to `(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x` where `L = [l₁, l₂, ..., lₙ]`.
More concisely: For any list `L` of lists and any element `x` of type `α`, the list expressions `x ++ (l₁ ++ x ++ ... ++ lₙ ++ x)` and `(x ++ l₁) ++ (x ++ l₂) ++ ... ++ (x ++ lₙ) ++ x` are equal, where `L = [l₁, l₂, ..., lₙ]`.
|
List.drop_take_succ_eq_cons_get
theorem List.drop_take_succ_eq_cons_get :
∀ {α : Type u_1} (L : List α) (i : Fin L.length), List.drop (↑i) (List.take (↑i + 1) L) = [L.get i]
This theorem states that for any list `L` of elements of any type `α` and any valid index `i` within the list, if you take the first `i+1` elements of the list and then drop the first `i` elements from this subset, you are left with a list of length `1` that consists solely of the `i`-th element from the original list `L`. In other words, it describes a method of extracting the `i`-th element from a list by first taking a subset of the list and then dropping elements.
More concisely: For any list `L` of length `n+1` and any index `i` where `0 ≤ i < n`, the sublist `L.take(i+1).drop(i)` equals the singleton list containing the `i`-th element of `L`.
|
List.join_filter_not_isEmpty
theorem List.join_filter_not_isEmpty :
∀ {α : Type u_1} {L : List (List α)}, (List.filter (fun l => !l.isEmpty) L).join = L.join
This theorem states that for any type `α` and any list `L` of lists of type `α`, if you filter out the empty lists from `L` and then concatenate all the remaining lists, the result is the same as if you simply concatenated all the lists in `L` directly. In other words, empty lists do not contribute to the final concatenated list. This property holds regardless of the specific type `α` of the list elements.
More concisely: For any type `α` and list `L` of lists of type `α`, the filtered list `L.filter (λ l, l.nonempty)` and the concatenation of `L` yield the same result.
|
List.drop_take_succ_eq_cons_nthLe
theorem List.drop_take_succ_eq_cons_nthLe :
∀ {α : Type u_1} (L : List α) {i : ℕ} (hi : i < L.length), List.drop i (List.take (i + 1) L) = [L.nthLe i hi] := by
sorry
This theorem states that for any list `L` of some type `α` and any natural number `i` such that `i` is less than the length of `L`, if we first take the first `i+1` elements of `L` and then drop the first `i` elements of this sublist, we will be left with a list that contains a single element. This element is precisely the `i`-th element of the original list `L`.
More concisely: For any list `L` of length `n+1` and natural number `i` with `0 <= i < n`, the sublist of `L` consisting of its first `i+1` elements, followed by the drop of its first `i` elements, equals the single-element list containing the `i`-th element of `L`.
|