List.nodup_iff_nthLe_inj
theorem List.nodup_iff_nthLe_inj :
∀ {α : Type u} {l : List α},
l.Nodup ↔ ∀ (i j : ℕ) (h₁ : i < l.length) (h₂ : j < l.length), l.nthLe i h₁ = l.nthLe j h₂ → i = j
The theorem `List.nodup_iff_nthLe_inj` states that for any list `l` of elements of an arbitrary type `α`, the condition of the list having no duplicate elements (`List.Nodup l`) is equivalent to the condition that, for any two indices `i` and `j` which are less than the length of the list (`i < List.length l` and `j < List.length l`), if the elements at index `i` and `j` are the same (`List.nthLe l i h₁ = List.nthLe l j h₂`), then `i` and `j` must be the same. In other words, no two distinct indices point to the same element in a list with no duplicates.
More concisely: For any list `l` of distinct elements, if `i` and `j` are indices such that `0 <= i, j < List.length l` and `List.nthLe l i = List.nthLe l j`, then `i = j`.
|
Mathlib.Data.List.Nodup._auxLemma.2
theorem Mathlib.Data.List.Nodup._auxLemma.2 : ∀ {α : Type u}, [].Nodup = True
The theorem `Mathlib.Data.List.Nodup._auxLemma.2` states that for all types `α`, an empty list of type `α` has no duplicates. In other words, the property of having no duplicates is always true for an empty list, regardless of the specific type of its elements.
More concisely: The empty list has no duplicates for any type α.
|
List.nodup_singleton
theorem List.nodup_singleton : ∀ {α : Type u} (a : α), [a].Nodup
The theorem `List.nodup_singleton` states that for any type `α` and for any element `a` of that type, a list consisting of just `a` has no duplicates. This is true by definition, since a list with a single element cannot have duplicate entries.
More concisely: For any type `α` and element `a` of that type, the list `[a]` has no duplicate elements.
|
List.nodup_cons
theorem List.nodup_cons : ∀ {α : Type u} {a : α} {l : List α}, (a :: l).Nodup ↔ a ∉ l ∧ l.Nodup
The theorem `List.nodup_cons` states that for any type `α`, and for any element `a` of this type and list `l` of elements of this type, the list `l` has no duplicates (i.e., the proposition `List.Nodup (a :: l)` holds) if and only if `a` is not an element of `l` and `l` itself has no duplicates (expressed as `a ∉ l ∧ List.Nodup l`).
More concisely: For any type `α` and list `l` of distinct elements of type `α`, `a` not being an element of `l` is equivalent to `l` having no duplicates.
|
List.nodup_iff_injective_get
theorem List.nodup_iff_injective_get : ∀ {α : Type u} {l : List α}, l.Nodup ↔ Function.Injective l.get
The theorem `List.nodup_iff_injective_get` states that for any type `α` and any list `l` of type `α`, the list `l` has no duplicate elements if and only if the function `List.get l` is injective. In other words, a list `l` is duplicate-free precisely when each index in the list `l` corresponds to a unique element, meaning that if two indices provide the same element, those two indices must be the same.
More concisely: A list of type `α` has no duplicate elements if and only if the function `List.get` on that list is injective.
|
Mathlib.Data.List.Nodup._auxLemma.4
theorem Mathlib.Data.List.Nodup._auxLemma.4 : ∀ {α : Type u} {a : α} {l : List α}, (a :: l).Nodup = (a ∉ l ∧ l.Nodup)
This theorem states that, for any type `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, the property that the list formed by prepending `a` to `l` has no duplicates (i.e., `List.Nodup (a :: l)`) is equivalent to the conjunction of the properties that `a` is not in `l` and `l` has no duplicates (i.e., `a ∉ l ∧ List.Nodup l`). In other words, a list has no duplicates if and only if its first element is not in the rest of the list and the rest of the list also has no duplicates.
More concisely: For any type `α` and list `l` of elements of type `α`, the list `a :: l` has no duplicates if and only if `a ∉ l` and `l` have no duplicates.
|
List.Nodup.map
theorem List.Nodup.map :
∀ {α : Type u} {β : Type v} {l : List α} {f : α → β}, Function.Injective f → l.Nodup → (List.map f l).Nodup := by
sorry
This theorem states that for any given type `α` and `β`, a list `l` of type `α`, and a function `f` from `α` to `β`, if the function `f` is injective (meaning that identical outputs imply identical inputs) and the list `l` has no duplicate elements (each element appears at most once in the list), then the list resulting from mapping the function `f` over `l` (applying `f` to each element of `l`) will also have no duplicate elements.
More concisely: If `f` is an injective function from type `α` to type `β` and list `l` of type `α` has no duplicates, then the list obtained by applying `f` to each element in `l` also has no duplicates.
|
List.Nodup.of_attach
theorem List.Nodup.of_attach : ∀ {α : Type u} {l : List α}, l.attach.Nodup → l.Nodup
This theorem, `List.Nodup.of_attach`, is an alias for the forward direction of `List.nodup_attach` in Lean 4. It states that for any list `l` of elements of any type `α`, if the "attached" version of `l` (i.e., `l.attach`) has no duplicate elements (i.e., is a "NoDup" list), then the original list `l` also has no duplicate elements (i.e., is a "NoDup" list).
More concisely: If `l.attach` is a NoDup list, then `l` is also a NoDup list.
|
List.Nodup.map_on
theorem List.Nodup.map_on :
∀ {α : Type u} {β : Type v} {l : List α} {f : α → β},
(∀ x ∈ l, ∀ y ∈ l, f x = f y → x = y) → l.Nodup → (List.map f l).Nodup
The theorem `List.Nodup.map_on` states that for any types `α` and `β`, and for any list `l` of type `α`, and any function `f` from `α` to `β`, if it holds that for all elements `x` and `y` in `l`, `f(x)` equals `f(y)` implies `x` equals `y`, then if `l` is a list with no duplicate elements, the list resulting from applying the function `f` to each element of `l` will also be a list with no duplicate elements. In other words, applying a function to each element of a list preserves the property of having no duplicate elements under the condition that the function gives distinct results for distinct elements.
More concisely: If `f : α -> β` preserves equality on distinct elements of a list `l` of type `α` with no duplicates, then the image list `map f l` also has no duplicates.
|
List.Nodup.of_map
theorem List.Nodup.of_map : ∀ {α : Type u} {β : Type v} (f : α → β) {l : List α}, (List.map f l).Nodup → l.Nodup := by
sorry
This theorem states that for any types `α` and `β`, and for any function `f : α → β`, if a list `l` of type `α` doesn't have any duplicates after applying the function `f` to each of its elements (i.e., the list obtained by `List.map f l` has no duplicates), then it can be concluded that the original list `l` itself also doesn't have any duplicates. In other words, no-duplication is preserved under the mapping operation.
More concisely: If `f : α -> β` is a function without duplicates on the list `l : List α`, then `l` itself is a list without duplicates.
|
Mathlib.Data.List.Nodup._auxLemma.5
theorem Mathlib.Data.List.Nodup._auxLemma.5 : ∀ {a b : Prop}, (a ∧ b) = (b ∧ a)
This theorem states that for all propositions 'a' and 'b', the conjunction 'a AND b' is equivalent to 'b AND a'. This is basically asserting the commutativity property of logical conjunction in propositional logic. In mathematical terms, if you have two conditions or properties 'a' and 'b', the statement " 'a' and 'b' are true" is the same as the statement " 'b' and 'a' are true".
More concisely: For all propositions a and b, the conjunction a AND b is equivalent to the conjunction b AND a.
|
List.nodup_iff_sublist
theorem List.nodup_iff_sublist : ∀ {α : Type u} {l : List α}, l.Nodup ↔ ∀ (a : α), ¬[a, a].Sublist l
This theorem states that for any type `α` and any list `l` of type `α`, the list `l` has no duplicates if and only if for every element `a` of type `α`, it is not the case that the sublist `[a, a]` (i.e., the list with two occurrences of `a`) is a sublist of `l`. In other words, a list has no duplicate elements if there are no elements `a` that appear consecutively in the list.
More concisely: A list of type `α` has no duplicates if and only if no sublist of length 2 contains an element repeated twice.
|
List.Nodup.pairwise_of_forall_ne
theorem List.Nodup.pairwise_of_forall_ne :
∀ {α : Type u} {l : List α} {r : α → α → Prop}, l.Nodup → (∀ a ∈ l, ∀ b ∈ l, a ≠ b → r a b) → List.Pairwise r l
This theorem states that for any type `α`, given a list `l` of type `α` and a binary relation `r` on `α`, if the list `l` has no duplicates (i.e., every element appears at most once in the list), and if for every distinct pair of elements `a` and `b` in `l`, `r a b` holds, then the elements of `l` are pairwise related by `r`. In other words, `r` holds for every pair of distinct elements in the list `l`.
More concisely: Given a list `l` of distinct elements of type `α` and a binary relation `r` on `α`, if `r` holds between every pair of distinct elements in `l`, then `r` holds for all pairs of distinct elements in `l`.
|
List.Nodup.attach
theorem List.Nodup.attach : ∀ {α : Type u} {l : List α}, l.Nodup → l.attach.Nodup
This theorem, `List.Nodup.attach`, states that for any list `l` of elements of some type `α`, if `l` doesn't have any duplicate elements (i.e., `l` is "nodup"), then the list obtained by attaching `l` also doesn't have any duplicate elements. This is an alias of the reverse direction of the theorem `List.nodup_attach`. In other words, it guarantees that the operation of attaching a list preserves the property of having no duplicate elements.
More concisely: If `l` is a nodup list of type `α`, then the list obtained by attaching to `l` is also nodup.
|
List.nodup_map_iff
theorem List.nodup_map_iff :
∀ {α : Type u} {β : Type v} {f : α → β} {l : List α}, Function.Injective f → ((List.map f l).Nodup ↔ l.Nodup) := by
sorry
The theorem `List.nodup_map_iff` states that for any two types `α` and `β`, a function `f` from `α` to `β`, and a list `l` of type `α`, if the function `f` is injective (meaning that if `f x = f y` then `x = y`), then the list `l` has no duplicate elements if and only if the list resulting from applying `f` to each element of `l` also has no duplicate elements. In other words, the uniqueness of the elements in the original list is preserved under the action of an injective function.
More concisely: For any injective function `f` and list `l`, if `l` has no duplicate elements then the list `[f x | x ∈ l]` also has no duplicate elements.
|
List.nodup_reverse
theorem List.nodup_reverse : ∀ {α : Type u} {l : List α}, l.reverse.Nodup ↔ l.Nodup
This theorem states that for any list `l` of elements of any type `α`, the list `l` has no duplicates if and only if the reverse of list `l` has no duplicates. This implies that reversing a list does not change its property of having no duplicate elements.
More concisely: For any list `l` of elements from type `α`, the list `l` has no duplicates if and only if its reverse `rev l` has no duplicates.
|
List.Nodup.sublist
theorem List.Nodup.sublist : ∀ {α : Type u} {l₁ l₂ : List α}, l₁.Sublist l₂ → l₂.Nodup → l₁.Nodup
The theorem `List.Nodup.sublist` states that for all types `α` and for any two lists `l₁` and `l₂` of type `α`, if `l₁` is a sublist of `l₂` and if `l₂` has no duplicates (expressed as `List.Nodup l₂`), then `l₁` also has no duplicates (expressed as `List.Nodup l₁`). In other words, if a list has no duplicate items, then any sublist of that list also has no duplicate items.
More concisely: If `l₁` is a sublist of `l₂` and `List.Nodup l₂`, then `List.Nodup l₁`.
|
List.nodup_attach
theorem List.nodup_attach : ∀ {α : Type u} {l : List α}, l.attach.Nodup ↔ l.Nodup
This theorem, `List.nodup_attach`, states that for any type `α` and any list `l` of that type, the property of the list `l` having no duplicates (expressed as `List.Nodup l`) is equivalent to the attached list of `l` (expressed as `List.attach l`) having no duplicates. Here, "having no duplicates" means each element in the list appears at most once. The process of "attaching" to a list involves creating a new list with the same elements but each element in the new list also carries a proof that it belongs to the original list.
More concisely: For any type `α`, the list `l` has no duplicates if and only if its attached list `List.attach l` has no duplicates.
|
List.nodup_nil
theorem List.nodup_nil : ∀ {α : Type u}, [].Nodup
This theorem states that an empty list, regardless of its type `α`, always has no duplicates. In other words, the property of having no duplicates, or `List.Nodup`, is always satisfied by an empty list.
More concisely: For all types `α`, the empty list of type `List α` has no duplicates.
|
List.nodup_append
theorem List.nodup_append : ∀ {α : Type u} {l₁ l₂ : List α}, (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂
The theorem `List.nodup_append` states that for all types `α` and for any two lists `l₁` and `l₂` of type `α`, the condition that the list formed by appending `l₁` and `l₂` has no duplicates (i.e., `List.Nodup (l₁ ++ l₂)`) is equivalent to the conjunction of three conditions: `l₁` has no duplicates (`List.Nodup l₁`), `l₂` has no duplicates (`List.Nodup l₂`), and `l₁` and `l₂` have no elements in common (`List.Disjoint l₁ l₂`). In other words, the concatenation of two lists is a list without duplicates if and only if both original lists are without duplicates and they do not share any common elements.
More concisely: For all types `α`, the list `l₁ ++ l₂` has no duplicates if and only if both `l₁` and `l₂` have no duplicates and are disjoint.
|
List.nodup_iff_count_le_one
theorem List.nodup_iff_count_le_one :
∀ {α : Type u} [inst : DecidableEq α] {l : List α}, l.Nodup ↔ ∀ (a : α), List.count a l ≤ 1
The theorem `List.nodup_iff_count_le_one` states that for any type `α` with a decidable equality and for any list `l` of type `α`, the property that the list `l` has no duplicates (signified by `List.Nodup l`) is equivalent to the condition that for every element `a` of type `α`, the count of `a` in the list `l` is less than or equal to one. This means that an element can appear at most once in the list if the list has no duplicates.
More concisely: For any type `α` with decidable equality and any list `l` of type `α`, `List.Nodup l` if and only if for all `a` in `α`, the count of `a` in `l` is less than or equal to one.
|
List.Nodup.not_mem
theorem List.Nodup.not_mem : ∀ {α : Type u} {l : List α} {a : α}, (a :: l).Nodup → a ∉ l
The theorem `List.Nodup.not_mem` states that for any type `α`, any list `l` of type `α`, and any element `a` of type `α`, if the list that is formed by appending `a` to the front of `l` has no duplicates (i.e., `List.Nodup (a :: l)`), then `a` is not a member of `l` (i.e., `a ∉ l`). This means that the condition of having no duplicates in the extended list ensures that the added element `a` is not already present in the original list `l`.
More concisely: If `a` is not a duplicate in the list `a :: l`, then `a` is not an element of `l`.
|
List.count_eq_one_of_mem
theorem List.count_eq_one_of_mem :
∀ {α : Type u} [inst : DecidableEq α] {a : α} {l : List α}, l.Nodup → a ∈ l → List.count a l = 1
This theorem states that for any type `α` with a decidable equality relation and any element `a` of this type, if `a` is a member of a list `l` of elements of type `α` and this list `l` has no duplicates (therefore each element appears at most once in the list), then the number of occurrences of `a` in `l` is exactly 1. In other words, if we have a list with no duplicates and an element is in that list, it must appear exactly once.
More concisely: For any type `α` with decidable equality and any list `l` of distinct elements of type `α`, the size of the subset of `l` equal to an element `a` is equal to 1 if and only if `a` is in `l`.
|