Mathlib.Data.List.Infix._auxLemma.11
theorem Mathlib.Data.List.Infix._auxLemma.11 : ∀ {α : Type u_1} (s t : List α), (s ∈ t.inits) = s.IsPrefix t
This theorem states that for any two lists `s` and `t` of some type `α`, `s` is an element of the list of tails of `t` if and only if `s` is a suffix of `t`. In other words, the list `s` appears as the last few elements of `t` exactly when `s` is one of the terminal segments of `t`. The `<:+` operator in Lean is used to express the "is a suffix of" relation.
More concisely: For any list `s` and `t` of type `α`, `s` is a suffix of `t` if and only if `s` is an element of the list of tails of `t`.
|
List.isSuffix.reverse
theorem List.isSuffix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsSuffix l₂ → l₁.reverse.IsPrefix l₂.reverse := by
sorry
This theorem, `List.isSuffix.reverse`, is an alias of the reverse direction of `List.reverse_prefix`. Given any type `α` and two lists `l₁` and `l₂` of type `α`, it states that if `l₁` is a suffix of `l₂`, then the reverse of `l₁` is a prefix of the reverse of `l₂`. In other words, if you have a list `l₂` and a sublist `l₁` that comes at the end of `l₂`, then if you reverse both lists, `l₁` will now come at the start of `l₂`.
More concisely: If `l₁` is a suffix of `l₂`, then the reverses of `l₁` and `l₂` are reversed prefixes of each other.
|
List.length_tails
theorem List.length_tails : ∀ {α : Type u_1} (l : List α), l.tails.length = l.length + 1
This theorem states that for any list `l` of elements of an arbitrary type `α`, the length of the list of all terminal segments of `l` (obtained using the `List.tails` function) is equal to the length of the original list plus one. The "+1" accounts for the empty list which is always included as the last element in the list of terminal segments.
More concisely: The number of terminal segments in a list of length n is equal to n+1.
|
List.eq_nil_of_suffix_nil
theorem List.eq_nil_of_suffix_nil : ∀ {α : Type u_1} {l : List α}, l.IsSuffix [] → l = []
This theorem, `List.eq_nil_of_suffix_nil`, states that for any type `α` and any list `l` of that type, if the list `l` is a suffix of an empty list, then `l` must be an empty list itself. This is a specific alias of the forward direction of the more general theorem `List.suffix_nil`.
More concisely: For any type `α`, if list `l` is a suffix of the empty list, then `l` is empty.
|
List.isPrefix.reverse
theorem List.isPrefix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsPrefix l₂ → l₁.reverse.IsSuffix l₂.reverse := by
sorry
This theorem, `List.isPrefix.reverse`, describes a property of lists. It states that for any type `α` and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a prefix of `l₂`, then the reverse of `l₁` is a suffix of the reverse of `l₂`. That is, reversing the lists maintains the relative position of `l₁` to `l₂`, but at the opposite end of the list.
More concisely: If list `l₁` is a prefix of list `l₂`, then the reversed list `reverse l₁` is a suffix of the reversed list `reverse l₂`.
|
List.eq_nil_of_infix_nil
theorem List.eq_nil_of_infix_nil : ∀ {α : Type u_1} {l : List α}, l.IsInfix [] → l = []
This theorem, called `List.eq_nil_of_infix_nil`, states that for any list `l` of any type `α`, if an empty list is an infix of `l`, then `l` must be an empty list. In other words, if a list contains an empty list as a continuous subsequence somewhere within it, the only way this can be true is if the original list is also empty.
More concisely: If a list `l` of type `α` contains an infix of length 0 (i.e., an empty list), then `l` is equal to the empty list.
|
List.eq_nil_of_prefix_nil
theorem List.eq_nil_of_prefix_nil : ∀ {α : Type u_1} {l : List α}, l.IsPrefix [] → l = []
This theorem, `List.eq_nil_of_prefix_nil`, states that for any list `l` of type `α`, if `l` is a prefix of an empty list, then `l` must be an empty list. In other words, the only list that can begin another list which has no elements is also a list with no elements.
More concisely: If a list `l` is a prefix of the empty list, then `l` is empty.
|
List.inits_eq_tails
theorem List.inits_eq_tails :
∀ {α : Type u_1} (l : List α), l.inits = (List.map List.reverse l.reverse.tails).reverse
This theorem states that for any given list `l` of a particular type `α`, the list of initial segments of `l` (as given by `List.inits l`) is the same as the list of reversed terminal segments of the reversed `l` (as given by `List.reverse (List.map List.reverse (List.tails (List.reverse l)))`). In simpler terms, it tells that if you reverse the list and take its terminal segments and then reverse those segments and the whole list again, you will get the initial segments of the original list.
More concisely: For any list `l` of type `α`, the list of initial segments `List.inits l` is equal to the list of reversed terminal segments of the reversed list `List.reverse l`, i.e., `List.reverse (List.map List.reverse (List.tails (List.reverse l)))`.
|
List.isInfix.reverse
theorem List.isInfix.reverse : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.IsInfix l₂ → l₁.reverse.IsInfix l₂.reverse := by
sorry
This theorem, `List.isInfix.reverse`, is an alias of the reverse direction of `List.reverse_infix`. It states that for all types `α`, and for all lists `l₁` and `l₂` of type `α`, if `l₁` is an infix of `l₂`, then the reverse of `l₁` is an infix of the reverse of `l₂`. In simpler terms, if a list `l₁` can be found inside `l₂` in the same order, then the reverse of `l₁` can also be found inside the reverse of `l₂` in the same order.
More concisely: For all types `α` and lists `l₁` and `l₂` of type `α`, if `l₁` is an infix of `l₂`, then `reverse l₁` is an infix of `reverse l₂`.
|