List.le_of_mem_argmax
theorem List.le_of_mem_argmax :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder β] {f : α → β} {l : List α} {a m : α},
a ∈ l → m ∈ List.argmax f l → f a ≤ f m
The theorem `List.le_of_mem_argmax` states that for any types `α` and `β`, where `β` has a linear order, and for any function `f` from `α` to `β`, any list `l` of elements of type `α`, and any elements `a` and `m` of type `α`, if `a` is an element of `l` and `m` is an element returned by the `argmax` function when applied to `f` and `l`, then the value of `f` at `a` is less than or equal to the value of `f` at `m`. In simpler terms, it asserts that the value of the function at any element in a list is less than or equal to the value of the function at the maximum element of the list, where the maximum is determined by the `argmax` function.
More concisely: For any type `α` and `β` with a linear order, and any function `f` from `α` to `β`, if `a` is an element in list `l` of type `α` and `m` is the `argmax` element of `f` and `l`, then `f a ≤ f m`.
|
List.maximum_ne_bot_of_length_pos
theorem List.maximum_ne_bot_of_length_pos :
∀ {α : Type u_1} [inst : LinearOrder α] {l : List α}, 0 < l.length → l.maximum ≠ ⊥
The theorem `List.maximum_ne_bot_of_length_pos` states that for any list `l` of elements of any type `α` that has a linear order structure, if the length of this list is greater than zero, then the maximum value of the list is not `⊥` (bottom). In other words, if a list is not empty, it will always have a maximum value.
More concisely: For any non-empty list `l` of elements with a linear order structure, the maximum element exists in `l`.
|
List.maximum_cons
theorem List.maximum_cons :
∀ {α : Type u_1} [inst : LinearOrder α] (a : α) (l : List α), (a :: l).maximum = max (↑a) l.maximum
The theorem `List.maximum_cons` states that for any type `α` that has a `LinearOrder` structure, any element `a` of type `α`, and any list `l` of elements of type `α`, the maximum element of the list that results from prepending `a` to `l` is the maximum of `a` and the maximum element of `l`. The maximum of `a` and the maximum element of `l` is computed using the `max` function, and the maximum element of the list is computed using the function `List.maximum`. If `l` is an empty list, the maximum of `a` and `List.maximum l` is simply `a`.
More concisely: For any type `α` with a `LinearOrder` structure and any list `l` of `α` elements, `max (a :: l) = max a (List.maximum l)`.
|
List.argmax_mem
theorem List.argmax_mem :
∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] [inst_1 : DecidableRel fun x x_1 => x < x_1] {f : α → β}
{l : List α} {m : α}, m ∈ List.argmax f l → m ∈ l
The theorem `List.argmax_mem` states that for any types `α` and `β`, provided `β` has a preorder (a binary relation indicating one element is less than or equal to another) and a decidable relation for less than, and given a function `f` from `α` to `β` and a list of elements of type `α`, if an element `m` of type `α` is the result of the function `List.argmax` applied to `f` and the list, then `m` must be an element of the original list. In other words, `List.argmax` always returns an element from the original list.
More concisely: For any type `α`, function `f` from `α` to a type `β` with a decidable less-than relation, and list `xs` of elements from `α`, if `m` is the argmax value of `f` over `xs`, then `m` is an element of `xs`.
|