List.duplicate_iff_sublist
theorem List.duplicate_iff_sublist : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l ↔ [x, x].Sublist l := by
sorry
This theorem, `List.duplicate_iff_sublist`, states that for any type `α` and any list `l` of type `α`, and any element `x` of type `α`, the element `x` is a duplicate in the list `l` if and only if the sublist `[x, x]` is a sublist of `l`. This is the contrapositive of the `List.nodup_iff_sublist` theorem.
More concisely: For any type `α` and list `l` of type `α`, an element `x` is a duplicate in `l` if and only if `[x, x]` is a sublist of `l`.
|
Mathlib.Data.List.Duplicate._auxLemma.4
theorem Mathlib.Data.List.Duplicate._auxLemma.4 :
∀ {α : Type u_1} {l : List α} {x y : α}, List.Duplicate x (y :: l) = (y = x ∧ x ∈ l ∨ List.Duplicate x l) := by
sorry
This theorem, named `_auxLemma.4` from the `Mathlib.Data.List.Duplicate` module in Lean, states that for any type `α`, any list `l` of type `α`, and any `x` and `y` of type `α`, the condition of `x` being a duplicate in the list formed by prepending `y` to `l` is equivalent to either `y` being equal to `x` and `x` being in `l`, or `x` being a duplicate in `l`.
More concisely: For any type `α`, list `l` of type `α`, and `x`, `y` of type `α`, `x` is a duplicate in the list `x :: y :: l` if and only if `y = x` or `x` is a duplicate in `l`.
|
List.Mem.duplicate_cons_self
theorem List.Mem.duplicate_cons_self : ∀ {α : Type u_1} {l : List α} {x : α}, x ∈ l → List.Duplicate x (x :: l) := by
sorry
This theorem states that, for any type `α`, any list `l` of type `α`, and any element `x` of type `α`, if `x` belongs to the list `l`, then `x` is a duplicate in the list constructed by consing `x` onto `l`. In other words, if an element is in a list, then adding that element to the front of the list will always result in a list where that element is duplicated.
More concisely: For any type `α`, if `x ∈ list α` then `x :: list α` contains a duplicate element.
|
List.Duplicate.mem
theorem List.Duplicate.mem : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l → x ∈ l
This theorem states that for any type 'α', any list 'l' of that type, and any element 'x' of that type, if 'x' is a duplicate in 'l' then 'x' is indeed an element of 'l'. In other words, if an element is duplicated in a list, it, therefore, must be a member of that list.
More concisely: For any type 'α' and list 'l' of length greater than 0 in 'α', if 'l' contains a duplicate element 'x', then 'x' is a member of 'l'.
|