List.nodup.of_sublists'
theorem List.nodup.of_sublists' : ∀ {α : Type u} {l : List α}, l.sublists'.Nodup → l.Nodup
This theorem is an alias for the forward direction of `List.nodup_sublists'`. It states that for any list `l` of a certain type `α`, if no two different sublists of `l` are the same (i.e., `l.sublists'.Nodup`), then the list `l` itself does not have any duplicate elements (`l.Nodup`).
More concisely: If the sublists of a list have no duplicates, then the list itself has no duplicate elements.
|
List.sublists'_eq_sublists
theorem List.sublists'_eq_sublists :
∀ {α : Type u} (l : List α), l.sublists' = List.map List.reverse l.reverse.sublists
This theorem states that for any list of type `α`, the list of all non-contiguous sublists generated by `sublists'` function is equivalent to the list of all reversed non-contiguous sublists generated by the `sublists` function applied to the reversed original list. In other words, if we reverse each non-contiguous sublist of the reversed original list, and collect these sublists using the `sublists` function, we will get the same result as if we had used the `sublists'` function on the original list.
More concisely: For any list `xs` of type `α`, the sets of non-contiguous sublists of `xs` and the reversed non-contiguous sublists of the reversed list `list.reverse xs` are equal.
|
Mathlib.Data.List.Sublists._auxLemma.4
theorem Mathlib.Data.List.Sublists._auxLemma.4 : ∀ {α : Type u} {s t : List α}, (s ∈ t.sublists') = s.Sublist t := by
sorry
The theorem `Mathlib.Data.List.Sublists._auxLemma.4` states that for any type `α` and any lists `s` and `t` of type `α`, `s` is a member of the list of all (non-contiguous) sublists of `t` (as generated by `List.sublists'`) if and only if `s` is a sublist of `t`. Here, a sublist means a sequence of elements from the original list in the original order but not necessarily contiguous.
More concisely: The theorem `Mathlib.Data.List.Sublists._auxLemma.4` in Lean 4 asserts that for all types `α` and lists `s` and `t` of `α`, `s` is a sublist of `t` if and only if `s` is a non-contiguous sublist of `t` as generated by `List.sublists'`.
|
List.sublistsLen_succ_cons
theorem List.sublistsLen_succ_cons :
∀ {α : Type u_1} (n : ℕ) (a : α) (l : List α),
List.sublistsLen (n + 1) (a :: l) = List.sublistsLen (n + 1) l ++ List.map (List.cons a) (List.sublistsLen n l)
This theorem asserts that for any given type `α`, an integer `n`, an element `a` of type `α` and a list `l` of type `α`, the list of all sublists of length `n + 1` of the list formed by prepending `a` to `l` can be obtained by appending the result of mapping the function that prepends `a` to each sublist of length `n` of `l` to the list of all sublists of length `n + 1` from `l`. In other words, every sublist of length `n + 1` from the list formed by adding `a` to `l` is either a sublist of `l` of the same length or a sublist of `l` of length `n` with `a` added to it.
More concisely: For any type `α`, list `l` of length `n` in `α`, and element `a` in `α`, the set of sublists of length `n+1` of the list `[a] ++ l` is the set of sublists of length `n+1` from `l` together with the sublists of length `n` from `l` with `a` appended.
|
List.sublists_append
theorem List.sublists_append :
∀ {α : Type u} (l₁ l₂ : List α),
(l₁ ++ l₂).sublists = do
let x ← l₂.sublists
List.map (fun x_1 => x_1 ++ x) l₁.sublists
The theorem `List.sublists_append` states that for any two lists `l₁` and `l₂` of the same type `α`, the list of all sublists of the concatenation of `l₁` and `l₂` is equivalent to the list generated by taking each sublist `x` of `l₂`, and then mapping each sublist of `l₁` to the concatenation of that sublist with `x`. This theorem describes a property of how the sublists of concatenated lists relate to the sublists of the original lists.
More concisely: The set of sublists of the concatenation of lists `l₁` and `l₂` is equal to the image of the set of sublists of `l₁` under the function that maps each sublist to its concatenation with `l₂`.
|
List.nodup_sublists
theorem List.nodup_sublists : ∀ {α : Type u} {l : List α}, l.sublists.Nodup ↔ l.Nodup
The theorem `List.nodup_sublists` states that for any type `α` and list `l` of type `α`, the list of all non-contiguous sublists of `l` has no duplicate elements if and only if the original list `l` has no duplicate elements. In other words, a list and its sublists share the property of either having no duplicate elements or not. This theorem connects the "no duplicates" property of a list to the "no duplicates" property of its sublists.
More concisely: For any type `α` and list `l` of length `n` over `α`, the list of non-contiguous sublists of `l` has no duplicate elements if and only if `l` itself has no duplicate elements (has length equal to its cardinality).
|
List.sublistsLen_zero
theorem List.sublistsLen_zero : ∀ {α : Type u_1} (l : List α), List.sublistsLen 0 l = [[]]
This theorem states that for any list `l` of any type `α`, the list of all sublists of `l` that are of length `0` is a list containing only the empty list. This is because a sublist of length `0` can only be an empty list, and there is exactly one empty list in any list.
More concisely: The set of sublists of any list `l` of length `0` is a singleton set containing only the empty list.
|
List.mem_sublists'
theorem List.mem_sublists' : ∀ {α : Type u} {s t : List α}, s ∈ t.sublists' ↔ s.Sublist t
This theorem states that for any lists `s` and `t` of any type `α`, `s` is a member of the list of all non-contiguous sublists of `t` (`List.sublists' t`) if and only if `s` is a sublist of `t` (`List.Sublist s t`). In other words, it establishes the equivalence between the membership of `s` in the list of all non-contiguous sublists of `t` and the sublist relationship of `s` to `t`.
More concisely: The theorem asserts that a list `s` is a non-contiguous sublist of list `t` if and only if `s` is a sublist of `t`.
|
List.nodup_sublists'
theorem List.nodup_sublists' : ∀ {α : Type u} {l : List α}, l.sublists'.Nodup ↔ l.Nodup
The theorem `List.nodup_sublists'` states that for any given list `l` of an arbitrary type `α`, the list `l` has no duplicates if and only if the list of all non-contiguous sublists of `l` also has no duplicates. In other words, a list and its sublists share the same "no duplicate" property. This means, if any element appears at most once in `l`, then in the list of all non-contiguous sublists of `l`, each sublist also appears at most once, and vice versa.
More concisely: For any list `l` of type `α`, `l` has no duplicates if and only if every non-contiguous sublist of `l` also has no duplicates.
|
List.pairwise_sublists
theorem List.pairwise_sublists :
∀ {α : Type u} {R : α → α → Prop} {l : List α},
List.Pairwise R l → List.Pairwise (fun l₁ l₂ => List.Lex R l₁.reverse l₂.reverse) l.sublists
The theorem `List.pairwise_sublists` states that for all types `α` and a binary relation `R` on `α`, given a list `l` of type `α`, if `l` is pairwise related under `R`, then all sublists of `l` are pairwise related under a new relation. This new relation is defined as the lexicographic order `List.Lex R` of the reverse of any two sublists. Being pairwise related under `R` means that for every pair of distinct elements in the list, the relation `R` holds. The lexicographic order of two lists is the order determined by the first position where the lists differ. In other words, the theorem ensures that the order property is preserved even after reversing and taking all possible non-contiguous sublists.
More concisely: If a list of pairwise related elements under a relation R, then all its non-contiguous sublists are pairwise related under the lexicographic order List.Lex(R) of their reversals.
|
List.sublists'_cons
theorem List.sublists'_cons :
∀ {α : Type u} (a : α) (l : List α), (a :: l).sublists' = l.sublists' ++ List.map (List.cons a) l.sublists' := by
sorry
The theorem `List.sublists'_cons` states that for all types `α` and any element `a` of type `α` and list `l` of type `List α`, the list of all non-contiguous sublists of the list resulting from prepending `a` to `l` (`a :: l`) is equal to the concatenation of the list of all non-contiguous sublists of `l` and the result of mapping the function `List.cons a` (which prepends `a` to its argument list) over the list of all non-contiguous sublists of `l`. This essentially means that every sublist of `a :: l` either is a sublist of `l`, or is formed by adding `a` to the start of a sublist of `l`.
More concisely: For all types `α` and lists `l` of `α`, the sublists of `a :: l` are exactly the sublists of `l` together with the lists obtained by prefixing `a` to each sublist of `l`.
|
List.map_ret_sublist_sublists
theorem List.map_ret_sublist_sublists : ∀ {α : Type u} (l : List α), (List.map List.ret l).Sublist l.sublists := by
sorry
This theorem states that for any list `l` of a general type `α`, the list obtained by applying the function `List.ret` (which maps each element of `l` to a list containing just that element) is a sublist of the list of all non-contiguous sublists of `l`. In other words, if you map each element of `l` to a list containing just that element, every resulting list will also appear in the list of all possible sublists of `l`.
More concisely: For any list `l` of type `α`, the image of `l` under the function `List.ret` is a subcollection of the set of all non-contiguous sublists of `l`.
|
List.sublists'_reverse
theorem List.sublists'_reverse : ∀ {α : Type u} (l : List α), l.reverse.sublists' = List.map List.reverse l.sublists
This theorem states that for any list `l` of elements of some type `α`, the list of all non-contiguous sublists of the reversed list `l` (obtained using `List.sublists'`) is equal to the list obtained by applying the reverse operation to each of the non-contiguous sublists of the original list `l` (obtained using `List.sublists`). In other words, reversing a list before or after extracting its non-contiguous sublists, but adjusting for the different sublist orderings, results in the same list of sublists.
More concisely: For any list `l` of elements `α`, the list of non-contiguous sublists of the reversed list `l` is equal to the list obtained by reversing each non-contiguous sublist of `l`.
|
List.nodup.sublists'
theorem List.nodup.sublists' : ∀ {α : Type u} {l : List α}, l.Nodup → l.sublists'.Nodup
This theorem, `List.nodup.sublists'`, states that for any list `l` of a generic type `α`, if `l` has no duplicate elements (i.e., `l.Nodup`), then any sublists of `l` generated using the `sublists'` function will also have no duplicate elements (`l.sublists'.Nodup`). It's essentially a formal proof in Lean 4 that ensuring the original list is free of duplicates will guarantee that the sublists derived from it are also free of duplicates.
More concisely: If `l` is a list with no duplicate elements, then every sublist of `l` also has no duplicate elements.
|
List.nodup.of_sublists
theorem List.nodup.of_sublists : ∀ {α : Type u} {l : List α}, l.sublists.Nodup → l.Nodup
This theorem, `List.nodup.of_sublists`, asserts that if the list of all sublists of a given list `l` contains no duplicate elements, then the original list `l` itself also contains no duplicate elements. Here, `l` is a list of elements of an arbitrary type `α`. In other words, if there are no repeated sublists in the list of all sublists, it implies that there are no repeated elements in the original list.
More concisely: If every sublist of list `l` has no repeated elements, then list `l` itself has no repeated elements.
|
List.length_sublists'
theorem List.length_sublists' : ∀ {α : Type u} (l : List α), l.sublists'.length = 2 ^ l.length
This theorem states that, for any list 'l' of type 'α', the length of the list of all its non-contiguous sublists generated by the function 'List.sublists'' is equal to 2 raised to the power of the length of the original list 'l'. In other words, given a list, the total number of its non-contiguous sublists is 2^n, where n is the length of the list.
More concisely: The number of non-contiguous sublists of a list of length n is 2^n.
|
List.nodup.sublists
theorem List.nodup.sublists : ∀ {α : Type u} {l : List α}, l.Nodup → l.sublists.Nodup
This theorem states that for any type `α` and for any list `l` of type `α`, if `l` has no duplicate elements (i.e., `l` is a "NoDup" list), then the list of all sublists of `l` also has no duplicate elements. In other words, there won't be any repeated sublists in the list of all sublists of `l`. It is an alias of the reverse direction of `List.nodup_sublists`.
More concisely: If `α` is a type and `l : list α` has no duplicates, then the list of all sublists of `l` also has no duplicates.
|