List.mem_dlookup_iff
theorem List.mem_dlookup_iff :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)},
l.NodupKeys → (b ∈ List.dlookup a l ↔ ⟨a, b⟩ ∈ l)
The theorem `List.mem_dlookup_iff` states that for any types `α` and `β` with `β` being a dependent type on `α`, given an instance of decidable equality for type `α`, a value `a` of type `α`, a value `b` of the dependent type `β a`, and a list `l` of `Sigma β` (key-value pairs with keys of type `α` and values dependent on keys), if the list `l` has no duplicate keys, then the value `b` is in the result of looking up the key `a` in `l` if and only if the pair `{ fst := a, snd := b }` is in the list `l`. In other words, this theorem connects the process of looking up a key-value pair in a list with no duplicate keys with the membership of the pair in the list itself.
More concisely: For lists without duplicate keys, `a` is in the key of the pair `{fst := a, snd := b}` in a list `l` of key-value pairs if and only if that pair is in `l`.
|
List.nodupKeys_cons
theorem List.nodupKeys_cons :
∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)},
(s :: l).NodupKeys ↔ s.fst ∉ l.keys ∧ l.NodupKeys
This theorem states that for any type `α`, a type `β` that is a function of `α`, a `Sigma β` object `s`, and a list of `Sigma β` objects `l`, the list has no duplicate keys (`List.NodupKeys`) when `s` is added to the front of `l` (`s :: l`) if and only if the first component of `s` (`s.fst`) is not in the list of keys of `l` (`List.keys l`) and `l` itself has no duplicate keys (`List.NodupKeys l`). In other words, a list of key-value pairs has distinct keys if each key is unique and none of them repeats in the remaining list.
More concisely: For any type `α` and lists `l` and `[s]` of `Σβα` pairs, `l` has no duplicate keys when `s` is prepended if and only if the first component of `s` is not in the keys of `l` and `l` is itself key-unique.
|
List.dlookup_kerase_ne
theorem List.dlookup_kerase_ne :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a a' : α} {l : List (Sigma β)},
a ≠ a' → List.dlookup a (List.kerase a' l) = List.dlookup a l
This theorem states that for any types `α` and `β`, assuming `α` has decidable equality, for any elements `a` and `a'` of type `α` and any list `l` of pairs where the first element is of type `α` and the second element's type depends on the first element, if `a` and `a'` are not equal, then looking up the element `a` in the list `l` after removing the first pair with key `a'` yields the same result as looking up `a` in the original list `l`. In other words, removing a pair with a different key does not affect the result of looking up `a`.
More concisely: Given types `α` with decidable equality, lists `l` of pairs `(α × β)` such that the first component is of type `α`, and elements `a` and `a'` of type `α`, if `a ≠ a'`, then looking up `a` in list `l` after removing the first pair with key `a'` is equal to looking up `a` in the original list `l`.
|
List.mem_keys_of_mem
theorem List.mem_keys_of_mem :
∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)}, s ∈ l → s.fst ∈ l.keys
This theorem states that for any type `α` and for any type `β` that is dependent on `α`, and for any sigma type `s` (which is a type of key-value pair) and any list `l` of sigma types, if `s` is an element of `l`, then the first component of `s` (which is the key in the key-value pair) is an element of the list of keys of `l`. In other words, if a key-value pair is in a list, then its key is in the list of keys.
More concisely: If a sigma type `s` with key `α` is an element of a list `l` of sigma types, then `α` is an element of the list of keys of `l`.
|
List.dlookup_cons_ne
theorem List.dlookup_cons_ne :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β),
a ≠ s.fst → List.dlookup a (s :: l) = List.dlookup a l
The theorem `List.dlookup_cons_ne` states that for any types `α` and `β`, where `β` is a dependent type determined by `α`, and for any list `l` of sigma types `β`, and any sigma type `s`, if the key `a` is not equal to the first component of `s`, then the result of the `dlookup` function (which finds the first value in the list corresponding to the key `a`) is the same whether we are looking in the list where `s` is the first element or in the original list `l`. In other words, if we're looking for a key that's not the key of the first element, prepending that first element won't affect the result of the `dlookup` function.
More concisely: For any types `α` and `β`, list `l` of sigma types `β`, and sigma type `s` with different keys, the result of `dlookup` on list `l` is equal to the result of `dlookup` on list `[s] ++ l`.
|
Mathlib.Data.List.Sigma._auxLemma.2
theorem Mathlib.Data.List.Sigma._auxLemma.2 :
∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)},
(s :: l).NodupKeys = (s.fst ∉ l.keys ∧ l.NodupKeys)
The theorem `Mathlib.Data.List.Sigma._auxLemma.2` states that for any type `α`, any dependent type `β` that depends on `α`, any element `s` of the dependent pair type `Sigma β`, and any list `l` of elements of `Sigma β`, it is true that `s` is a distinct key in the list `s :: l` if and only if the first element of `s` (i.e., `s.fst`) is not in the keys of `l` and all keys in `l` are distinct (`List.NodupKeys l`).
More concisely: For any type `α` and dependent type `β`, given an element `s` of the dependent pair type `Σβ`, and a list `l` of pair elements of `Σβ` where all keys are distinct, `s` is the unique key in `s :: l` if and only if the first element of `s` is not a key in `l`.
|
List.not_mem_keys_of_nodupKeys_cons
theorem List.not_mem_keys_of_nodupKeys_cons :
∀ {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)}, (s :: l).NodupKeys → s.fst ∉ l.keys
This theorem states that for any type `α`, any type `β` which depends on `α`, any `s` of type `Sigma β`, and any list `l` of type `Sigma β`, if the list created by prepending `s` to `l` does not contain duplicate keys (`List.NodupKeys (s :: l)`), then the first element of `s` (i.e., `s.fst`) is not in the list of keys of `l` (`s.fst ∉ List.keys l`). Essentially, if a list of key-value pairs has no duplicate keys, the key of the first pair is not a key in the rest of the list.
More concisely: If `s :: l` is a list of key-value pairs such that `List.NodupKeys (s :: l)`, then `s.fst` is not a key in `l`.
|
List.kerase_cons_eq
theorem List.kerase_cons_eq :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)},
a = s.fst → List.kerase a (s :: l) = l
The theorem `List.kerase_cons_eq` states that for any type `α` that has decidable equality, any type function `β` from `α` to some type, any value `a` of type `α`, any pair `s` in the sigma type of `β`, and any list `l` of pairs in the sigma type of `β`, if `a` is equal to the first element of the pair `s`, then removing the first pair in the list `l` whose first element is `a` from the list that has `s` added to the front of `l` results in the original list `l`. In other words, if `a` is the key of the first pair in the list, then removing the first pair with key `a` will result in the rest of the list.
More concisely: For any decidably equal type `α`, if `a` equals the first element of pair `s` in the sigma type of a type function `β` and `l` is a list of such pairs, then removing the first pair `s` from `l` and adding it to the front of `l` results in the original list `l` without the pair containing `a`.
|
List.mem_dlookup_kunion
theorem List.mem_dlookup_kunion :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)},
b ∈ List.dlookup a (l₁.kunion l₂) ↔ b ∈ List.dlookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ List.dlookup a l₂
The theorem `List.mem_dlookup_kunion` states that for all types `α` and `β`, given the decidable equality on `α`, and for any `a` of type `α`, `b` of type `β a`, and `l₁` and `l₂` being lists of key-value pairs (Sigma types), the value `b` is in the list obtained by looking up the key `a` in the list formed by the key-union of `l₁` and `l₂` if and only if `b` is in the list obtained by looking up `a` in `l₁`, or `a` is not a key in `l₁` and `b` is in the list obtained by looking up `a` in `l₂`. In other words, this theorem describes the behavior of the `dlookup` operation with respect to the `kunion` operation on lists of key-value pairs.
More concisely: For all types `α` and `β`, given decidable equality on `α`, the key `a` is in the list obtained by key-union of `l₁` and `l₂` if and only if it is in `l₁` or is not in `l₁` but is in the value associated with `a` in `l₂`.
|
List.kerase_of_not_mem_keys
theorem List.kerase_of_not_mem_keys :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
a ∉ l.keys → List.kerase a l = l
This theorem states that for any type `α`, a dependent type `β` that depends on `α`, and an instance of decidable equality on `α`, given a key `a` of type `α` and a list `l` of key-value pairs (sigmas), if the key `a` is not found in the list of keys derived from `l`, then the list obtained by removing the first occurrence of the key `a` from `l` (using the `List.kerase` function) is equal to the original list `l`. In other words, removing a key that is not present in the list of key-value pairs doesn't change the list.
More concisely: For any type `α`, if `a` is not an element of the list `l` of key-value pairs `(α × β) list`, then `l` is equal to the list obtained by removing the first occurrence of the pair `(a, _)` from `l` using `List.kerase`.
|
List.nodupKeys_iff_pairwise
theorem List.nodupKeys_iff_pairwise :
∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)}, l.NodupKeys ↔ List.Pairwise (fun s s' => s.fst ≠ s'.fst) l
This theorem states that for any list `l` of Sigma types, indexed by a type function `β` on a type `α`, the list has no duplicate keys if and only if for every pair of elements `s` and `s'` in the list, the first components of `s` and `s'` (usually the keys in the context of a key-value pair) are not equal. In terms of the data structure, this means that the list behaves like a map or a dictionary, where no two elements share the same key.
More concisely: For any list of pairs (α × β) indexed by β, the list has no duplicate keys if and only if the projection of the first component of each pair in the list are pairwise distinct.
|
List.dlookup_cons_eq
theorem List.dlookup_cons_eq :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a),
List.dlookup a (⟨a, b⟩ :: l) = some b
The theorem `List.dlookup_cons_eq` states that for any types `α` and `β`, assuming `α` has a decidable equality, given a list `l` of Sigma types (`Sigma β`), a value `a` of type `α`, and a value `b` of type `β a`, when we prepend a pair with first element `a` and second element `b` to the list `l` and then look for the first value in the new list that corresponds to the key `a` using `List.dlookup`, we will always get the value `b`. Essentially, this theorem asserts that `List.dlookup` correctly retrieves the most recently added value for a given key in a list of key-value pairs.
More concisely: Given a list `l` of pairs `(α × β)`, an element `a` of type `α`, and its corresponding element `b` of type `β` in this list, `List.dlookup (a :: l) = b`.
|
Mathlib.Data.List.Sigma._auxLemma.14
theorem Mathlib.Data.List.Sigma._auxLemma.14 : ∀ {a : Prop}, (¬¬a) = a
This theorem, named `Mathlib.Data.List.Sigma._auxLemma.14`, states that for any type `α`, given it has an addition operation, a less or equal to relation, is covariant in its operation, and is contravariant in its operation, for any elements `a`, `b`, and `c` of type `α`, the statement `(a + b ≤ a + c)` is equivalent to `(b ≤ c)`. In simpler words, if you have two quantities `b` and `c`, and you add the same value `a` to both of them, the inequality relationship between `b` and `c` remains the same.
More concisely: For any type `α` with covariant and contravariant addition and a reflexive, transitive less-than or equal relation, `(a + b ≤ a + c)` if and only if `(b ≤ c)`.
|
List.kerase_cons_ne
theorem List.kerase_cons_ne :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)},
a ≠ s.fst → List.kerase a (s :: l) = s :: List.kerase a l
The theorem `List.kerase_cons_ne` states that for any type `α`, type `β` that is a function of `α`, a decidable equality instance for `α`, and given an element `a` of type `α`, a pair `s` of type `Sigma β`, and a list `l` of pairs of type `Sigma β`, if `a` is not equal to the first element of the pair `s`, then the operation of key erasure `List.kerase` on `a` from the list that is the result of appending `s` and `l`, is equal to the list that is the result of appending `s` and the list obtained by applying `List.kerase` on `a` from `l`. In other words, if `a` is not the key of the pair at the head of the list, it is not removed and the `List.kerase` operation continues on the rest of the list.
More concisely: For any type `α`, function type `β -> α`, decidable equality instance for `α`, element `a` of `α`, pair `s` of type `Σβ`, and list `l` of pairs of type `Σβ`, if `a ≠ fst s`, then `List.kerase a (s :: l) = s :: List.map (λ x => (fst x, List.kerase (fst x) (snd x :: l))) l`.
|
List.NodupKeys.kerase
theorem List.NodupKeys.kerase :
∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)} [inst : DecidableEq α] (a : α),
l.NodupKeys → (List.kerase a l).NodupKeys
The theorem `List.NodupKeys.kerase` states that for all types `α` and `β` with `β` being a dependent type on `α`, for all lists `l` of pairs (key-value pairs, represented as `Sigma β`), and any element `a` of type `α`, if the list `l` satisfies the property `List.NodupKeys` (meaning that the keys in the list do not duplicate), then the list resulting from the operation `List.kerase a l` (which removes the first pair with the key `a` from the list `l`) also satisfies the property `List.NodupKeys`. The equality of keys is decidable, which is represented by the `DecidableEq α` instance.
More concisely: If `l` is a list of key-value pairs `(α × β)` with no duplicate keys (`List.NodupKeys l`), then the list obtained by removing the key-value pair with key `a` (`List.kerase a l`) also has no duplicate keys.
|
List.dlookup_isSome
theorem List.dlookup_isSome :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
(List.dlookup a l).isSome = true ↔ a ∈ l.keys
This theorem, `List.dlookup_isSome`, states that for any type `α` with decidable equality, and for any dependent type `β` indexed by `α`, for all elements `a` of type `α` and for all lists `l` of key-value pairs where the keys are of type `α` and the values are of the type `β` indexed by the corresponding key, the statement "the option returned by `List.dlookup` of `a` in `l` is not `none`" is equivalent to "the element `a` is in the list of keys of `l`". In other words, a key `a` is in the list of keys of `l` if and only if looking up `a` in the list `l` using `List.dlookup` returns some value rather than `none`.
More concisely: For any type `α` with decidable equality and dependent type `β` indexed by `α`, the option returned by `List.dlookup` on list `l` of key-value pairs with keys of type `α` and values of type `β` indexed by keys, is `some (β a)` for some `a` in `α` if and only if `a` is an element of the list of keys.
|
List.keys_kerase
theorem List.keys_kerase :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)},
(List.kerase a l).keys = l.keys.erase a
This theorem states that for any type α, for a function β from α to another type, for a list 'l' of key-value pairs where the type α has decidable equality, and for any key 'a' of type α, the list of keys obtained after removing the first pair with key 'a' from 'l' (using the function `List.kerase`) is the same as the list obtained by first getting the list of keys from 'l' and then removing the key 'a' from this list (using the function `List.erase`). In other words, the order of the operations 'get keys' and 'remove key' does not matter.
More concisely: For any type α with decidable equality, any function β from α to another type, and list 'l' of key-value pairs in α, the lists obtained by removing the first pair with key 'a' from 'l' using `List.kerase` and by first getting the list of keys from 'l' and then removing key 'a' using `List.erase` are equal.
|
List.lookup_ext
theorem List.lookup_ext :
∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {l₀ l₁ : List (Sigma β)},
l₀.NodupKeys → l₁.NodupKeys → (∀ (x : α) (y : β x), y ∈ List.dlookup x l₀ ↔ y ∈ List.dlookup x l₁) → l₀.Perm l₁
This theorem, `List.lookup_ext`, states that for any two lists of sigma types, `l₀` and `l₁`, with keys from a type `α` and values from a type dependent on `α`, given that `α` has decidable equality, if both lists have no duplicate keys (`List.NodupKeys l₀` and `List.NodupKeys l₁`), and for all keys `x` from `α` and their corresponding values `y`, `y` is in the lookup of `x` in `l₀` if and only if `y` is in the lookup of `x` in `l₁`, then `l₀` and `l₁` are permutations of each other (`List.Perm l₀ l₁`). In simpler terms, if two key-value lists have unique keys and equivalent lookups for every key-value pair, then they must be rearrangements of each other.
More concisely: If two lists of sigma types with decidable key equality and no duplicate keys have equivalent lookups for all keys, then they are permutations of each other.
|