List.duplicate_iff_exists_distinct_nthLe
theorem List.duplicate_iff_exists_distinct_nthLe :
∀ {α : Type u_1} {l : List α} {x : α},
List.Duplicate x l ↔
∃ n, ∃ (hn : n < l.length), ∃ m, ∃ (hm : m < l.length) (_ : n < m), x = l.nthLe n hn ∧ x = l.nthLe m hm
The theorem `List.duplicate_iff_exists_distinct_nthLe` states that an element `x` of type `α` is a duplicate in a list `l` of type `List α` if and only if there exist two distinct indices `n` and `m` (both of type `ℕ`) within the list `l` such that `x` is the element at both these indices. In other words, `x` is a duplicate element in the list `l` exactly when there are two distinct positions in the list that both contain `x`.
More concisely: An element `x` is a duplicate in list `l` if and only if there exist distinct indices `n` and `m` such that `l.get(n) = l.get(m) = x`.
|
List.duplicate_iff_exists_distinct_get
theorem List.duplicate_iff_exists_distinct_get :
∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l ↔ ∃ n m, ∃ (_ : n < m), x = l.get n ∧ x = l.get m := by
sorry
The theorem `List.duplicate_iff_exists_distinct_get` states that for any type `α`, any list `l` of type `List α`, and any element `x` of type `α`, the element `x` is a duplicate in the list `l` if and only if there exist two distinct indices `n` and `m` such that `n` is less than `m`, and the element at index `n` and the element at index `m` of the list `l` are both equal to `x`.
More concisely: For any list `l` and element `x`, `x` is a duplicate in `l` if and only if there exist distinct indices `n` and `m` such that `n < m` and `l.n = l.m = x`.
|
List.sublist_iff_exists_orderEmbedding_get?_eq
theorem List.sublist_iff_exists_orderEmbedding_get?_eq :
∀ {α : Type u_1} {l l' : List α}, l.Sublist l' ↔ ∃ f, ∀ (ix : ℕ), l.get? ix = l'.get? (f ix)
The theorem `List.sublist_iff_exists_orderEmbedding_get?_eq` states that for any two lists `l` and `l'` of a certain type `α`, `l` is a sublist of `l'` if and only if there exists an order-preserving embedding function `f` that maps natural numbers to natural numbers such that any element of `l` found at an index `ix` is also found at the index `f ix` in `l'`. This embedding basically re-indexes the elements in `l` to their corresponding indices in `l'`.
More concisely: A list `l` is a sublist of list `l'` if and only if there exists a bijective function `f` from the natural numbers to itself such that `l.i = l'.(f i)` for all indices `i` in the list `l`.
|
List.sublist_of_orderEmbedding_get?_eq
theorem List.sublist_of_orderEmbedding_get?_eq :
∀ {α : Type u_1} {l l' : List α} (f : ℕ ↪o ℕ), (∀ (ix : ℕ), l.get? ix = l'.get? (f ix)) → l.Sublist l'
This theorem states that if there exists an order-preserving embedding function `f` from natural numbers to natural numbers such that for any index `ix` of list `l`, the element found at `ix` in `l` is also found at index `f ix` in another list `l'`, then `l` is a sublist of `l'`. In other words, if you can map every element in `l` to its corresponding element in `l'` using an order-preserving embedding function, then `l` is a sublist of `l'`.
More concisely: If there exists an order-preserving function `f` such that for all `ix`, the `ix`-th element of list `l` is the same as the `f ix`-th element of list `l'`, then `l` is a sublist of `l'`.
|
List.sublist_iff_exists_fin_orderEmbedding_get_eq
theorem List.sublist_iff_exists_fin_orderEmbedding_get_eq :
∀ {α : Type u_1} {l l' : List α}, l.Sublist l' ↔ ∃ f, ∀ (ix : Fin l.length), l.get ix = l'.get (f ix)
This theorem states that a list `l` of type `α` is a sublist of another list `l'` of the same type if and only if there exists an order-preserving function `f` that embeds the finite set of indices of `l` into the finite set of indices of `l'`. This function should satisfy the property that for any index `ix` in `l`, the element of `l` at index `ix` is the same as the element of `l'` at index `f ix`.
More concisely: A list `l` is a sublist of list `l'` if and only if there exists a bijective function `f` from the finite index set of `l` to the finite index set of `l'` such that `l.(!(ix)) = l'.(!(f ix))` for all indices `ix` in `l`.
|