List.eq_or_mem_of_mem_cons
theorem List.eq_or_mem_of_mem_cons : ∀ {α : Type u_1} {a b : α} {l : List α}, a ∈ b :: l → a = b ∨ a ∈ l
This theorem states that for any type `α`, any two elements `a` and `b` of type `α`, and a list `l` of elements of type `α`, if `a` is an element of the list that consists of `b` followed by `l`, then `a` is either equal to `b` or `a` is an element of `l`. In other words, it underscores the fact that if an element is part of a list, it must be either the head of the list or part of the tail.
More concisely: For any type `α` and elements `a, b` of type `α`, if `a` is in the list `[b] :: l` (i.e., `a` is the head or an element of the list `l`), then `a` is equal to `b` or `a` is an element of `l`.
|
List.length_mapAccumr
theorem List.length_mapAccumr :
∀ {α : Type u} {β : Type v} {σ : Type w₂} (f : α → σ → σ × β) (x : List α) (s : σ),
(List.mapAccumr f x s).2.length = x.length
The theorem `List.length_mapAccumr` confirms that for any types `α`, `β`, and `σ`, and any function `f` of type `α → σ → σ × β`, list `x` of type `List α`, and value `s` of type `σ`, the length of the list obtained by applying the `List.mapAccumr` function with these parameters and taking the second element of the resulting pair equals the length of the original list `x`. This confirms that the `List.mapAccumr` operation maintains the length of the list.
More concisely: For any type `α`, `β`, and `σ`, and any function `f : α -> σ -> σ × β`, the length of the list obtained by applying `List.mapAccumr f x s` is equal to the length of the original list `x`.
|
List.length_le_of_sublist
theorem List.length_le_of_sublist : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₁.length ≤ l₂.length
This theorem, `List.length_le_of_sublist`, states that for any type `α` and any two lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂`, then the length of `l₁` is less than or equal to the length of `l₂`. Essentially, this theorem assures that the length of a sublist will always be less than or equal to the length of the list it's drawn from.
More concisely: For all types `α` and lists `l₁` and `l₂` of length `n₁` and `n₂` respectively with `l₁` being a sublist of `l₂`, we have `n₁ ≤ n₂`.
|
List.length_mapAccumr₂
theorem List.length_mapAccumr₂ :
∀ {α : Type u} {β : Type v} {φ : Type w₁} {σ : Type w₂} (f : α → β → σ → σ × φ) (x : List α) (y : List β) (c : σ),
(List.mapAccumr₂ f x y c).2.length = min x.length y.length
This theorem states that for any type of elements `α`, `β`, `φ`, and `σ`, and for any function `f` that takes elements of type `α`, `β`, and `σ` to produce a pair consisting of an element of type `σ` and `φ`, and given lists `x` and `y` of types `α` and `β`, respectively, and an element `c` of type `σ`, the length of the second element of the pair returned by the `List.mapAccumr₂` function applied to `f`, `x`, `y`, and `c` is equal to the minimum of the lengths of `x` and `y`. In other words, the length of the list resulting from a `mapAccumr₂` operation over two input lists is determined by the shortest of the two input lists.
More concisely: For any functions `f : α -> β * φ` and given lists `x : list α` and `y : list β` of lengths `|x|` and `|y|` respectively, the length of the second component of the pair returned by `List.mapAccumr₂ f x y` is `min |x| |y|`.
|